Computer-Aided Formal Reasoning
News
- update lecture notes (fix typo at Ackermann's method)
- Added material for SMT
- add links to agda code by Andreas Abel
- IMPORTANT: date and time of exam changed! (see below)
- upload paper on STA
- update lecture notes
- update lecture notes to cover new topics
- add Coq script and examples, tutorial is on Uniworx
- no tutorial on Fri 05/27
- date for exam
- new tutorial sheet on Uniworx
- add first batch of PVS examples
- corrected Thurday lecture time to: noon-2pm
- upload lecture notes
Contents
Computer-aided theorem proving means to carry out mathematical proofs
on a computer whose job it is to check steps, to perform bookkeeping
tasks and to automate routine steps. Conducting a proof on a computer
may be compared to and has a lot in common with implementing an
informally given algorithm or model.
Computer-Aided Formal Reasoning has numerous applications in software and hardware verification, as well as prototype development; and to a lesser extent in the formalization of "real" mathematical proofs.
The course covers theoretical foundations of computer aided formal reasoning in particular sequent calculus, type theory, automatic decision procedures, and demonstrates practical aspects using the theorem prover PVS. We also demonstrate alternative provers, in particular COQ and Spass. We will see case studies from hardware verification and also have two guest lectures from Keiko Nakata, FireEye, Dresden and Andreas Abel, U Gothenburg.
Organisation
- Volume: 3+2 academic hours per week, 6 ECTS
- Lecture and Tutorials: Prof. Martin Hofmann, Dr. Gordon Cichon
Place and Time
| Session | Time | Place | Begin |
|---|---|---|---|
| Lecture | Wed, 10am-noon | Richard-Wagner-Str. 10, room D 018 | 04/13/2016 |
| Lecture | Thu, noon-2pm | Theresienstr. 41, room C 112 | 04/14/2016 |
| Tutorials | Fri, 4pm-6pm | Oettingenstr. 67, room 161 | 04/22/2016 |
Schedule
Since there are 4 academic hours per week, and the course itself is only 3 hours per week, some lecture slots will be skipped. The tutorials will be contiguous.
Preliminary Schedule:
| Nr. | Date | Topic | Lecturer | Comments |
|---|---|---|---|---|
| 1. | 4/13 | Introduction | MH | PVS examples |
| 2. | 4/14 | Sequent calculus recap, PVS | MH | |
| 3. | 4/20 | Predicate logic (FOL) recap | MH | |
| 4. | 4/21 | FOL Metatheory: Herbrand's theorem, completeness, compactness | MH | |
| 4/27 4/28 5/4 5/5 |
no lecture | |||
| 5. | 5/11 | FOL and equality (also in PVS) | MH | |
| 6. | 5/12 | Inductive proofs for lists: filter, reverse sorting, etc. Other datatypes | GC | |
| 7. | 5/18 | Case study: ripple adder | GC | |
| 8. | 5/19 | Propositions as types, Coq | Jeremy Ledent, MH | |
| 5/25 5/26 |
no lecture | |||
| 9. | 6/1 | More experience with Coq | Jeremy Ledent, MH | Coq examples |
| 10. | 6/2 | Equational theories, universal models, convexity | MH | |
| 11. | 6/8 | Decision procedures for equality: Ackermann, Nelson-Oppen | MH | |
| 12. | 6/9 | Decision procedures for equality: canonisation | MH | |
| 13. | 6/15 | Solving equations, Shostak Light | MH | |
| 14. | 6/16 | Hardware verification | GC | |
| 15. | 6/22 | Case study: pipelined ALU | GC | |
| 16. | 6/23 | Case study, Formal Semantics of Synchronous Transfer Architecture | GC | paper |
| 17. | 6/29 | Guest Lecture | Keiko Nakato, FireEye, Dresden |
|
| 18. | 6/30 | Guest Lecture | Andreas Abel, Gothenburg | links to Agda code |
| 19. | 7/6 | Satisfiability modulo theories, Yices&Z3 | MH | yices, SMT, PocklingtonCertificates |
| 20. | 7/7 |
Integrating decision procedures via reflection |
MH | article |
| 21. | 7/13 | Q&A | MH, GC |
Exams
Exam
The exam will be an oral exam.
Date: 07/15 from 5pm till 7pm, Thursday 07/14 from noon till 2pm
Location: Theresienstr. 41, room C 112
Registration via Uniworx system.
Make-up Exam
tba.
Registration via Uniworx system.
Tutorials
Registration via Uniworx system.
- Tutorial 1: on Uniworx
- Tutorial 2: on Uniworx
Additional Information
PVS
SPASS
Literature
Document Actions