Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Theorem Proving Tools for Program Analysis

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:

  1. 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")
  2. Decidability:
    Describe the decidable classes of queries handled by the system.
  3. User Interaction and Guidance:
    Describe the user interaction model.
    How do users guide or otherwise control the tool search?
  4. 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.

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)