Formal Methods in Software Engineering
This course is an introduction to Model-Based Analysis and Testing techniques. 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 12:15, Liivi 2-612.
- Fridays 10:15, Liivi 2-612.
- Instructor: Vesal Vojdani (vesal@ut.ee)
- Mailing list: ati.fm@lists.ut.ee
- Exam:
- Home exam deadline: 14.01.2013
- Oral exam: 15.01.2013 (register timeslot!)
- Room: 512 (below the lecture room).
List of Topics
The following techniques and tools will be covered. The underlying theory, such as SAT/SMT solving, Büchi Automata and Abstract Interpretation, 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:
- Verification of Sequential Programs (Dafny)
- Static Analysis for Verifying Contracts (CodeContracts)
- Symbolic Execution for Test Generation (Pex)
- Model-Based Test Generation (SpecExplorer)
- Explicit State Model Checking (SPIN)
- Symbolic Model Checking (nuSMV)
- Model Checking Software: State bounds (CBMC) & Abstraction (SLAM)
- Static Analysis of Concurrent Systems (Goblint)
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."
Acknowledgements
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).
