CS-550 / 6 crédits

Enseignant: Kuncak Viktor

Langue: Anglais


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

Learning Prerequisites

Recommended courses

Computer Language Processing / Compilers

 

Important concepts to start the course

Discrete Mathematics

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

Teaching methods

Instructors will present lectures and exercises and supervise labs on student laptops.

 

Expected student activities

Follow the course material and complete and explain projects during the semester.

Assessment methods

The grade is based on the code, documentation, and explanation of projects during the semester.

There are no written exams.

Supervision

Office hours Yes
Assistants Yes
Forum Yes

Resources

Bibliography

  • 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
  • Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
  • 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

Websites

Moodle Link

Videos

Dans les plans d'études

  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Semestre: Automne
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines
  • Forme de l'examen: Pendant le semestre (session d'hiver)
  • Matière examinée: Formal verification
  • Cours: 2 Heure(s) hebdo x 14 semaines
  • Exercices: 2 Heure(s) hebdo x 14 semaines
  • TP: 2 Heure(s) hebdo x 14 semaines

Semaine de référence

 LuMaMeJeVe
8-9     
9-10     
10-11     
11-12     
12-13     
13-14     
14-15     
15-16     
16-17     
17-18     
18-19     
19-20     
20-21     
21-22