Formal Verification and Model Checking (212041-WS 24/25)

Description

Complex digital systems have an increasing presence and impact on our lives, making the formal verification of the correctness of these systems crucial. For instance, a spacecraft's program should not crash, and a networking system should stay operational even if one server goes down. To ensure this, one approach is deductive verification, involving the generation of a collection of logical constraints that the system must satisfy. These constraints can be algorithmically verified through automatic theorem provers such as SAT and SMT solvers. Another popular approach is model checking, which consists of representing the system via mathematical models and exhaustively checking certain properties, often described in temporal logics. This course covers various aspects of formal verification and model checking, including:

• Satisfiability of propositions: resolution and the main ingredients of modern satisfiability provers.
• Satisfiability modulo theories, in particular using linear inequalities, and the underlying simplex algorithm.
• Explicit-state and symbolic algorithms for model checking linear-time (LTL) and branching-time (CTL) temporal logics for finite machines.
• Symbolic model checking using BDDs.
• Model checking under probabilities and uncertainty, using Markov chains and Markov decision processes, with the logic PCTL and expected reward properties.
• The machine learning technique reinforcement learning, and model checking and formal verification techniques to render it safe to use on critical systems.

Learning Outcomes

After completing this course, the participants will be able to

• Solve practical verification problems using modern tools such as SAT/SMT solvers and model checkers like PRISM or Storm.
•  Understand algorithms underlying modern SAT and SMT solvers, such as resolution, CDCL, and CDCL(T).
• Understand formal logics such as LTL or CTL, and understand the algorithmic implications of model checking against such properties.
• Connect SAT and SMT methods to problems from classical planning, program verification, model checking, and probabilistic inference.
• Recognize situations in which the applications of model checking and verification techniques for specification and analysis may be useful.
• Work on cutting-edge research that combines machine learning and artificial intelligence with the rigorous techniques of formal verification.

Literature

• Christel Baier and Joost-Pieter Katoen. “Principles of model checking.” (2008).
• Daniel Kroening and Ofer Strichman. "Decision Procedures: An Algorithmic Point of View". (2008).