| Week 1 |
Tu 01/10 |
- Introduction
- Slides: [ppt
| pdf]
|
| Th 01/12 |
- Discussion of papers (please read before class):
- Logics: standard logics
- Slides: [ppt
| pdf]
|
| Week 2 |
Tu 01/17 |
- Logics: encoding computation in first-order logic
- Discussion of papers (read and writer reviews before
class):
- Flanagan, Leino, Lillibridge, Nelson, Saxe,
State, Extended
Static Checking for Java, PLDI 02 (read sections 1, 2, and 3)
- 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]
|
| Th 01/19 |
- Applications (Part I)
- Slides: [ppt]
|
| Week 3 |
Tu 01/24 |
- Applications (Part II)
- Slides: [ppt
| pdf]
|
| Th 01/26 |
- Finish ESC/Java
- Overview of search in the semantic domain
- Slides: [ppt]
|
| Week 4 |
Tu 01/31 |
- 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]
|
| Th 02/02 |
- Equality (Part I)
- Congruence closure/E-graph
- Quantifiers
- Skolemization
- Unification
- Matching
- Slides: [ppt]
|
| Week 5 |
Tu 02/07 |
- Decision procedures
- Communication between decision procedures
- Slides: [ppt]
|
| Th 02/09 |
- 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 02/14 |
- Search in the proof domain (Part II)
- sequent calculus
- tactics and tacticals
- Slides: [ppt]
|
| Th 02/16 |
- Mid-term project presentations
|
| Week 7 |
Tu 02/21 |
- Search in the proof domain (Part III)
- Slides: [ppt]
|
| Th 02/23 |
- Applications (Part III)
- Slides: [ppt]
|
| Week 8 |
Tu 02/28 |
- No lecture, instructor out of town
|
| Th 03/02 |
- Applications (Part IV)
- Guest lecture by Ranjit Jhala on predicate abstraction,
and using counter-examples productively
- Slides: [ppt]
|
| Week 9 |
Tu 03/07 |
- Equality (Part II)
- rewrite rules
- inductionless induction
- Slides: [ppt]
|
| Th 03/09 |
- 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.
- Slides: [ppt]
|
| Week 10 |
Tu 03/14 |
- Synthesizing Loop
Invariants
- Constructive logic, and Curry-Howard isomorphism
- extracting code from proofs, Coq, NuPRL
- Slides: [ppt]
|
| Th 03/16 |
- Final project presentations
|