ComputerAided 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: noon2pm
 upload lecture notes
Contents
Computeraided 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.
ComputerAided 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, 10amnoon  RichardWagnerStr. 10, room D 018  04/13/2016 
Lecture  Thu, noon2pm  Theresienstr. 41, room C 112  04/14/2016 
Tutorials  Fri, 4pm6pm  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, NelsonOppen  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.
Makeup 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