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 theorem provers:

• 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.

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