Formal Methods in Software Engineering (Version 0.3)
This course is an introduction to rigorous software development and quality assurance techniques. We study ways of gaining confidence (occasionally even mathematical certainty) that a software implementation does precisely what it's supposed to do. This naturally requires formal ways of specifying our intentions, including various logics and process models.
In this course, we will experiment with real tools as well as learn the underlying theory. Therefore, some of the lectures will be hands-on labs and rather informal, while others will be more conventional lectures, dry and without any sense of humor.
- Lectures / Labs:
- Wednesdays 16:15, Liivi 2-512.
- Fridays 10:15, Liivi 2-512.
- Vesal Vojdani (firstname.lastname@example.org)
- Kalmer Apinis (email@example.com)
List of Topics
The following techniques and tools will be covered, although some of it more superficially than others. The underlying theory will be introduced in a demand-driven fashion. Since the theory is a lot of fun in and of itself, we have to space things out to keep you motivated to hear all this practical stuff:
- Contract Checking (Contracts for Java, CodeContracts, Pex)
- Deductive Program Verification (Dafny, Why3, Z3)
- Interactive Theorem Proving (Coq)
- Verification of Object-Oriented Programs (KeY)
- Automated Program Verification (CPAChecker, Goblint)
- Modelling Concurrent Systems (SPIN) and Complex Structures (Alloy)
- Model-Based Test Generation (ModelJUnit)
More broadly, the essence of this course is best expressed by a famous quotation from the father of Social Psychology, Kurt Lewin: "There is nothing more practical than a good theory."
The preparation of this course was partially supported by the EU ARTEMIS Joint Undertaking under grant agreement n° 269335 (MBAT: Combined Model-based Analysis and Testing of Embedded Systems) and the German Research Foundation (DFG).