Program Verification

Main content

A hands-on introduction to the theory and construction of deductive software verifiers, covering both cutting-edge methodologies for formal program reasoning, and a perspective over the broad tool stacks making up modern verification tools.

Students will earn the necessary skills for designing and developing deductive verification tools which can be applied to modularly analyse complex software, including features challenging for reasoning such as heap-based mutable data and concurrency. Students will learn both a variety of fundamental reasoning principles, and how these reasoning ideas can be made practical via automatic tools.

Students will be gain practical experience with reasoning tools at various levels of abstraction, from SAT and SMT solvers at the lowest level, up through intermediate verification languages and tools, to verifiers which target front-end code in executable languages.

By the end of the course, students should have a good working understanding and experience of the issues and decisions involved with designing and building practical verification tools, and the theoretical techniques which underpin them.

The course will be organized around building up a "tool stack", starting at the lowest-level with background on SAT and SMT solving techniques, and working upwards through tools at progressively-higher levels of abstraction. The notion of intermediate verification languages will be explored, and the Boogie (Microsoft Research) and Viper (ETH) languages will be used in depth to tackle increasingly ambitious verification tasks.

The course will intermix technical content with hands-on experience; at each level of abstraction, we will build small tools on top which can tackle specific program correctness problems, starting from simple puzzle solvers (Soduko) at the SAT level, and working upwards to full functional correctness of application-level code. This practical work will include three mini-projects (each worth 10% of the final grade) spread throughout the course, which count towards the final grade. An oral examination (worth 70% of the final grade) will cover the technical content covered.

General info

Course catalogue: 263-2812-00L

Lecturer: Dr. Alexander Summers

Language: English

Hours: 2V1U

Credits: 4 credits

Prerequisites:
Some programming experience is essential, as the course contains several practical assignments. A basic familiarity with propositional and first-order logic will be assumed.

Courses with an emphasis on formal reasoning about programs (such as Formal Methods and Functional Programming) are advantageous background, but are not a requirement.

Lectures

Wednesday 9:00-11:00,  CAB G52, Dr. Alexander Summers

Dates Topics Downloads
22nd February (Week 1) Overview, SAT Solving Algorithms

Course Overview (PDF, 874 KB)

1. SAT Solving Algorithms (PDF, 1.4 MB)

1st March (Week 2) Encoding Problems to SAT 2. Encoding Problems to SAT (PDF, 1.7 MB)
8th March (Week 3) SMT Solving Algorithms 3. SMT Solving Algorithms (PDF, 1.3 MB)
15th March (Week 4) Quantifiers 4. Quantifiers (PDF, 1.5 MB)
22nd March (Week 5) Encoding to SMT

5. Encoding to SMT (PDF, 1.1 MB)

 

Pairs file from lecture (VPR, 572 Bytes)

 

Peano numbers file from lecture (VPR, 2 KB)

 

Sequences file from lecture (VPR, 813 Bytes)

29th March (Week 6) Hoare Logic and Weakest Preconditions 6. Hoare Logic and Weakest Preconditions (PDF, 1.4 MB)
5th April (Week 7) Advanced Verification Condition Generation 7. Advanced Verification Condition Generation (PDF, 1.2 MB)
12th April (Week 8) The Boogie Intermediate Verification Language 8. The Boogie Intermediate Verification Language (PDF, 1.9 MB)
3rd May (Week 10) Heap Reasoning and Permission Logics 9. Heap Reasoning and Permission Logics (PDF, 1.5 MB)
10th May (Week 11) Unbounded Heap Data

10. Unbounded Heap Data (PDF, 1.1 MB)

 

List examples from lecture (VPR, 3 KB)

 

Quantified Permissions examples from lecture (VPR, 4 KB)

17th May (Week 12) Advanced Specification and Verification

11. Advanced Specification and Verification (PDF, 1000 KB)

 

Set-To-Array example from lecture (VPR, 3 KB)

24th May (Week 13) Permissions and Concurrent Programs 12. Permissions and Concurrent Programs (PDF, 1.4 MB)
31st May (Week 14) Good Abstractions and Research Topics 13. Good Abstractions and Research Topics (PDF, 1.2 MB)

Exercises

Wednesday 11:00-12:00, CAB G52, Dr. Alexander Summers

 
 
Page URL: http://www.pm.inf.ethz.ch/education/courses/program-verification.html
23.06.2017
© 2017 Eidgenössische Technische Hochschule Zürich