Theorem prover (TP) accepts a logical formula and tries to prove that the formula is valid. Possible outcomes:

• TP says: “Yes, formula is valid”
• TP says: “No, formula is not valid, here is a counterexample which shows it is false”
• TP says: “I don't know. Too hard for me (within given time/memory)”
• TP loops forever

Example automated theorem provers:

• CVC3
• SMT-LIB Library and Competition

• SPASS from the Max Planck Institut for Computer Science
• E prover
• TPTP Library and Competition of Provers

Combine user insight with automated techniques.

User decomposes proof into pieces, the prover checks individual steps. Typically invokes automated theorem provers and other tactics to show the individual steps hold.

Example:

• Isabelle Theorem Prover
• Coq Proof Assistant - popular in programming languages community
• ACL2 Language and Prover - identifies a LISP subset with a logic

Decision procedure considers a smaller set of formulas, it always terminates and (given enough time) never says “I don't know”.

Example decidable classes of formulas:

• integer linear arithmetic (no multiplication of variables, only by constants)
• linear arithmetic over reals
• formulas of first-order logic, without quantifiers

Example theories for which no decision procedure exists:

• arithmetic with multiplication

Semidecision procedure: must terminate if answer is “yes”, need not terminate if answer is “no”.

• Example: first-order logic

Important question: combining different decision procedures and using them inside provers

• we will explore this question as well in this course

Recall the big picture in Verification as Science. What is the role of the theorem prover?

Role of prover in analysis: analyzer asks theorem prover questions

• with complex enough logic, entire program correctness becomes a theorem
  • program semantics tells us how this theorem looks like (we will see)
  • usually this theorem is very large and difficult, so not feasible to do automatically (but can use interactive provers)
  • program analyzers are specialized theorem provers - using knowledge of program structure to gain automation
• if user provides (loop) invariants, the problem reduces to multiple simple theorems
  • you will build in class systems that implement this reduction
• modern analyzers can internally call prover(s) many times to synthesize invariants and check that program satisfies desired property
  • you learn about examples of such systems