Multi-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. This research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem. This research contributes mechanisms that permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. It also contributes a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, this dissertation investigates the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced. / text

Establishing the termination of programs is a fundamental problem in the field of software verification. For transformational programs, termination is used to extend partial correctness to total correctness. For reactive systems, termination reasoning is used to establish liveness properties. In the context of theorem proving, termination is used to establish the consistency of definitional axioms and to automate proofs by induction. Of course, termination is an undecidable problem, as Turing himself proved. However, the question remains: how automatic can a general termination analysis be in practice? In this dissertation, we develop two new general frameworks for reasoning about termination and demonstrate their effectiveness in automating the task of proving termination in the domain of applicative first-order functional languages. The foundation of the first framework is the development of the first known complete set of algorithms for ordinal arithmetic over an ordinal notation. We provide algorithms for ordinal ordering ($<$), addition, subtraction, multiplication, and exponentiation on the ordinals up to epsilon-naught. We prove correctness and complexity results for each algorithm. We also create a library for automating arithmetic reasoning over epsilon-naught in the ACL2 theorem proving system. This ordinal library enables new termination proofs that were previously not possible in previous versions of ACL2. The foundation of the second framework is an algorithm for fully automating termination reasoning with no user assistance. This algorithm uses a combination of theorem proving and static analysis to create a Calling Context Graph (CCG), a novel abstraction that captures the looping behavior of the program. Calling Context Measures (CCMs) are then used to prove that no infinite path through the CCG can be an actual computation of the program. We implement this algorithm in the ACL2, and empirically evaluate its effectiveness on the regression suite, a collection of over 11,000 user-defined functions from a wide variety of applications.

Due to the difficulty of obtaining formal proofs, there is increasing interest in partially or completely automating proof search in interactive theorem provers. Despite being a theorem prover with an active community and plentiful corpus of 170,000+ theorems, no deep learning system currently exists to help automate theorem proving in ACL2. We have developed a machine learning system that generates recommendations to automatically complete proofs. We show that our system benefits from the copy mechanism introduced in the context of program repair. We make our system directly accessible from within ACL2 and use this interface to evaluate our system in a realistic theorem proving environment.

Les technologies actuelles permettent l'intégration sur une même puce de systèmes complexes (SoCs) qui sont composés de blocs préconçus (IPs) pouvant être interconnectés grâce à un réseau sur la puce (NoCs). De manière générale, les IPs sont validés par diverses techniques (simulation, test, vérification formelle) et le problème majeur reste la validation des infrastructures des communications. Cette thèse se concentre sur la vérification formelle des réseaux sur puce à l'aide d'un outil de preuve automatique, le démonstrateur de théorèmes ACL2. Un méta-modèle pour les réseaux sur puce a été développé et implémenté dans ACL2. Il satisfait des propriétés de correction générique, conséquences logiques d'un ensemble d'obligations de preuve sur les constituants principaux du réseau (topologie, routage, technique de commutation,...). La preuve de correction pour une instance spécifique de réseau sur puce est alors réduite à la vérification de ces obligations de preuve. Cette thèse poursuit les travaux entrepris dans ce domaine en étendant ce méta-modèle dans plusieurs directions : prise en compte plus fine de la modélisation temporelle, du contrôle de flux, des mécanismes de priorités,... Les résultats sont démontrés sur plusieurs réseaux actuels : Hermes (Université fédérale du Rio Grande do Sul, Brésil et LIRMM) et Nostrum (Royal Institute Of Technology, Suéde).