The tutorial will expose POPL attendees to several theorem proving tools and to help give them the ability to choose an appropriate tool for their specific application. The tutorial is presented by authors of current top theorem proving tools.

This tutorial will be co-located with POPL 2011, Austin, Texas.

## Which theorem prover fits my needs?

This question can be difficult to answer with exposure to only one or two theorem provers. Research and development into theorem proving technologies over the last few decades have given rise to a number of highly complementary theorem proving tools. This tutorial aims to provide answers to this question by assembling authors of set of top theorem proving systems. The theorem proving systems cover quite different areas:

- Computational logic
- Interactive theorem proving with integrated solvers
- SMT solving
- High performance pure SAT and QBF solvers
- Automatic first-order theorem provers

While each tool addresses significantly different problems, we will

as part of the tutorial identify a set of common themes that each

tool description will address:

**Logic:**

Describe the mathematical logic supported by the system.

(e.g., "propositional temporal logic",

"predicate calculus with induction but no quantifiers" or

"constructive type theory")**Decidability:**Describe the decidable classes of queries handled by the system.**User Interaction and Guidance:**

Describe the user interaction model.

How do users guide or otherwise control the tool search?**Main applications:**Describe which applications have so far driven the tools.

Each tutorial is to include a description of an application

with emphasis on scope of POPL.

### Tools

The tutorial will include tools from the list below.

- ACL2 http://userweb.cs.utexas.edu/users/moore/acl2/
- PVS http://pvs.csl.sri.com/
- Yices http://yices.csl.sri.com/
- Z3 http://research.microsoft.com/projects/z3
- Pico/Preco-SAT, Quantor (SAT/QBF): http://fmv.jku.at/picosat/, http://fmv.jku.at/precosat/, http://fmv.jku.at/quantor/
- Vampire:http://vprover.org

The tutorial will take place over 1 1/2 days prior to the POPL 2011 conference.

It will comprise of an interleaving of tool presentations and labs. The lab sessions will give the attendees an opportunity to get some hands on experience with the tools.

Related Tutorial on Isabelle

A related tutorial on Isabelle is planned in conjunction with POPL. It will give attendees an opportunity for in-depth exposure to Isabelle and we recommend this for exposure to LCF inspired proof assistants, which is not covered in this tutorial.

### Schedule

January 24-25, co-located with POPL 2011, Austin Texas

#### Monday January 24th

9-10:30 AM ACL2 J Strother Moore (UT Austin)

10:30-11 AM Break

11-12:30 PM PVS Natarajan Shankar (SRI International)

12:30-2 PM Lunch

2-3:30 PM Vampire Andrei Voronkov (U Manchester)

3:30-4 PM Break

4-5:30 PM SAT/QBF Armin Biere (Linz)

#### Tuesday January 25th

9-10:30 AM SMT Nikolaj Bjorner, Leonardo de Moura (Microsoft Research),

Bruno Dutertre (SRI International)

10:30-11 AM Break

11-12:30 PM Hands on lab All

12:30-2 PM Lunch

Tools and Reading Material:

ACL2 Slides

PicoSAT, PrecoSAT, DepQBF Examples Slides

PVS Tutorial, Course, Slides, Examples

Vampire,

Yices, Z3 Slides

### Workshop contacts:

Nikolaj Bjorner (Microsoft Research) nbjorner@microsoft.com, J Strother Moore (UT Austin), Ashish Tiwari (SRI International)