CSE 291: Applied Automated Theorem Proving

Spring Quarter, 2008

General information

Meeting times and location: T-Th 2:00-3:20, location: CENTER 204
Instructor: Sorin Lerner (email: my last name "at" cs.ucsd.edu, Office hours: by appointment)
Course syllabus and detailed Course topics.

Course project

Information about the mini-project can be found here
Information about the main project can be found here

Schedule (ever evolving)

Week 1	Tu 04/01	Introduction Slides: [ppt \| pdf]
Week 1	Th 04/03	Discussion of papers (please read before class): Demillo, Lipton, and Perlis, Social Processes and Proofs of Theorems and Programs, CACM 79 J Strother Moore, A Mechanized Program Verifier, talk at The Verification Grand Challenge Workshop, Zurich, October 10--13, 2005 Logics: standard logics Slides: [ppt \| pdf]
Week 2	Tu 04/08	Logics: encoding computation in first-order logic Discussion of papers (read and write reviews before class): Flanagan, Leino, Lillibridge, Nelson, Saxe, State, Extended Static Checking for Java, PLDI 02 Lerner, Millstein, Rice, Chambers, Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, POPL 05 (sections 1, 2, and 3) Also, don't worry if you don't understand all the details in what you read... We will go through the details in class. Slides: [ppt \| pdf]
Week 2	Th 04/10	Applications (Part I) Rhodium Slides: [ppt \| pdf]
Week 3	Tu 04/15	Applications (Part II) ESC/Java Slides: [ppt \| pdf]
Week 3	Th 04/17	Finish ESC/Java Overview of search in the semantic domain Slides: [ppt \| pdf]
Week 4	Tu 04/22	Search in the semantic domain DPLL using SAT solvers incrementally Martin Davis and Hilary Putnam, A Computing Procedure for Quantification Theory, JACM, 1960. 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 Slides: [ppt]
Week 4	Th 04/24	Equality (Part I) Congruence closure/E-graph G. Nelson and D. Oppen. Fast Decision Procedures Based on Congruence Closure. JACM, Vol 27, No 2, April 1980, pp. 356-364. 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 Slides: [ppt]
Week 5	Tu 04/29	Decision procedures Communication between decision procedures Greg Nelson and Derek C. Oppen Simplification by Cooperating Decision Procedures. TOPLAS, 1(2):245257, Oct 1979. Slides: [ppt]
Week 5	Th 05/01	Decision Procedures Communication between the heuristic prover and decision procedures Search in the proof domain (Part I) Hilbert-style systems natural decuction Slides: [ppt]
Week 6	Tu 05/06	Search in the proof domain (Part II) sequent calculus tactics and tacticals Slides: [ppt]
Week 6	Th 05/08	Search in the proof domain (Part III) resolution Slides: [ppt]