VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Formal Verification
Formal Verification (in English)
Last Updated: 2026-02-05 15:07:02
Abstract
The class covers the formal foundations and basic principles of algorithms used for verifying complex software automatically. We discuss SAT, BDDs, decision procedures, model checking and automatic abstraction.
Objective
Our goal is to introduce the basics of formal verification.
Content
The development of more and more powerful and complex software requires more sophisticated methods than traditional techniques to ensure functional correctness of the code. Currently, test engineers have to fight with a huge amount of simulation and test runs that cannot be handled any more. This effect is even more problematic in the light of shorter innovation cycles and the increasing pressure to react quickly to the market. One solution, if not the only alternative in the long run, is to consequently use automated formal methods. In particular, static analysis and model checking are becoming an integral part of the software development process. A market of commercial providers of formal tools is emerging. We will introduce the basics of three formal methods: Decision procedures, Model checking, and Automatic abstraction. There are no special requisites for this lecture, except that we expect some interest in formal approaches and algorithms.
General Information
- Language
- English
- Levels
- BSC , DS , MSC
- Frequency
- Yearly recurring
Examination
- Type
- end-of-semester examination
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Formal Verification (in English) |
|
2 h weekly |
| exercise | Formal Verification (in English) |
|
1 h weekly |