Formal verification
CS-550 / 8 credits
Teacher: Kuncak Viktor
Language: English
Remark: This course is a "depth" for Cyber Security master program and Cyber Security minor.
Summary
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.
Content
Tools used may include some of these: Stainless ( https://github.com/epfl-lara/stainless ), Lisa ( https://github.com/epfl-lara/lisa ) and Lean ( https://lean-lang.org/ ). Examinations may take place throughout the weeks during the entire semester, which may require substantial presence to pass the course.
Topics may include (among others) some of the following:
- Methodology of Formal Verification
- Review of Sets, Relations, Propositional and First-Order Logic
- Completeness and Semi-Decidability for First-Order Logic Proof Systems
- State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions.
- Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures
- Interactive Theorem Provers (Proof Assistants) such as Lisa and Lean
- SAT Solvers and Bounded Model Checking
- Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics
- Symbolic Execution. Satisfiability Modulo Theories
- Abstract Interpretation
Learning Prerequisites
Recommended courses
CS-320 Computer language processing
Important concepts to start the course
Discrete Mathematics (e.g. Kenneth Rosen: Discrete Mathematics and Its Applications)
Learning Outcomes
By the end of the course, the student must be able to:
- Formalize specifications
- Synthesize loop invariants
- Specify software functionality
- Generalize inductive hypothesis
- Critique current software development practices
- Formalize specifications
- Synthesize loop invariants
- Specify software functionality
- Generalize inductive hypothesis
- Critique current software development practices
Teaching methods
Instructors will present lectures and exercises and supervise labs on student laptops.
Expected student activities
Follow the course materials, take exams during the semester.
Assessment methods
The grade is based on the the exams carried out during the semester.
Supervision
| Office hours | Yes |
| Assistant.e.s | Yes |
| Forum | Yes |
Resources
Bibliography
- Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511576430
- Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
- Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
- Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Including Chapter Model Checking Security Protocols by David Basin.
- Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
- Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999.
- Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002.
- http://logitext.mit.edu/tutorial
Ressources en bibliothèque
Notes/Handbook
See sldes on course page
Websites
Prerequisite for
MSc thesis in the LARA group
In the programs
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: mandatory
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: mandatory
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: mandatory
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: During the semester (winter session)
- Subject examined: Formal verification
- Courses: 2 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional