CSE 291: Applied Automated Theorem Proving

Spring Quarter, 2010

General information

Meeting times and location: Tu-Th 12:30-1:50, location: SOLIS 111
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

Schedule (ever evolving)

Week 1	Tu 03/30	Introduction Slides: [ ppt \| pdf ]
Week 1	Th 04/01	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/06	Logics: encoding computation in first-order logic Slides: [ ppt \| pdf ]
Week 2	Th 04/08	Logics: Work on Mini-project together
Week 3	Tu 04/13	Applications, Part I: Rhodium and PEC Slides: [ ppt \| pdf ]
Week 3	Th 04/15	Applications, Part I (continued): Rhodium and PEC
Week 4	Tu 04/20	Applications (Part II) ESC/Java Slides: [ ppt \| pdf ]
Week 4	Th 04/22	Finish ESC/Java
Week 5	Tu 04/27	Overview of search in the semantic domain Slides: [ ppt \| pdf ]
Week 5	Th 04/29	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 \| pdf ]
Week 6	Tu 05/04	Intro to Coq
Week 6	Th 05/06	Intro to Coq (continued)
Week 7	Tu 05/11	Mini-project using Coq
Week 7	Th 05/13	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 \| pdf ]
Week 8	Tu 05/18	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 \| pdf ]
Week 8	Th 05/20