Links und Funktionen

You are here: Home / Teaching / Summer 2016 / Computer-Aided Formal Reasoning


Computer-Aided Formal Reasoning

Lecture 3 hours, Wed 10-12, Thu 12-14, Hofmann, Cichon; Tutorials, 2 hours, Cichon



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.


  • Volume: 3+2 academic hours per week, 6 ECTS
  • Lecture and Tutorials: Prof. Martin Hofmann, Dr. Gordon Cichon


Place and Time

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



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:

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
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
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

lecture notes
WIFT tutorial

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



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

Registration via Uniworx system.


 Registration via Uniworx system.

  • Tutorial 1: on Uniworx
  • Tutorial 2: on Uniworx


Additional Information




Document Actions