Course topics

Search

• Search in the proof domain
• natural deduction
• sequents
• resolution
• Search in the semantic domain
• DPLL
• using SAT solvers incrementally
  
  • P. C. Gilmore, A Proof Method for Quantification Theory: Its justification and Realization, IBM Journal of Research and Development, 1960
  Cormac Flanagan, Rajeev Goshi, Xinming Ou, and James B. Saxe, Theorem Proving using Lazy Proof Explication, CAV 03

Handling important aspects of first-order logic

• Quantifiers
  • Skolemization
  • Unification
  • Matching
    • David Detlefs, Greg Nelson and James B. Saxe, Simplify: a Theorem Prover for Program Checking, Journal of the ACM 52(3):365 - 473, 2005
    • David Detlefs, Greg Nelson and James B. Saxe, Simplify: a Theorem Prover for Program Checking, Technical Report, HP Labs
• Induction
  • induction based on recursive structure
    • Boyer and Moore, A computational logic, Academic Press, 1979, chapter XIV
    • Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, June, 2000.
  • inductionless induction
• Equality
  • Congruence closure/E-graph
  • Rewrite rules

Applications

• ESC/Java
  • Flanagan, Leino, Lillibridge, Nelson, Saxe, State, Extended Static Checking for Java, PLDI 02 (read sections 1, 2, and 3)
• Rhodium
  • Lerner, Millstein, Rice, Chambers, Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, POPL 05 (sections 1, 2, and 3)
• Predicate abstraction
  • Susanne Graf and Hassen Saidi, Construction of Abstract State Graphs of Infinite Systems with PVS, CAV 97
  • Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani, Automatic Predicate Abstraction of C Programs, PLDI 01
• Proof carrying code
• Curry-Howard isomorphism
  • Gurevich, Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand (handout will be given in class, with the sections you should read)