ACL2 Seminar, June 19, 2013
David Rager (joint work with Warren Hunt and Matt Kaufmann)

Title: A Parallelized Theorem Prover for a Logic with Parallel Execution

Abstract:

In order to take best advantage of modern multi-core systems,
interactive theorem provers need to parallelize execution effectively.
We describe our modification to a particular theorem prover, ACL2, to
use parallel execution automatically in its proof process.  Since the
ACL2 prover is written primarily in the ACL2 programming language, our
approach to parallelization takes advantage of ACL2 language
primitives for parallel execution.  We demonstrate that the resulting
system often provides earlier useful feedback from failed proofs and
significant reduction of execution time for successful proofs.  Thus,
our system not only incorporates parallelism into its proof process,
but it also provides a platform for writing and verifying parallel
programs written in the ACL2 programming language.