Today, software determines many areas of our daily lives. Some examples that most of us come into contact with on a daily basis are smartphone apps (e.g. for communicating with friends), software in ATMs, POS systems, smartcards and assistance systems in vehicles. For the above examples and many other applications, it is important that software functions correctly. For safety-critical systems, it is often not sufficient to test software: Testing can only reveal errors, but not prove the absence of errors. Instead, formal methods for specification and verification are used.
Software verification proves the correctness of an algorithm with respect to a formal requirement specification. In the proseminar, different approaches to the formal specification of software systems (e.g., automata, transition systems, and process algebras) and requirements for software systems (e.g., temporal logics) as well as methods for formal verification (e.g., model checking, theorem provers) are considered.
Literature / Links
- Visser, Havelund, Brat, Park: Model Checking Programs, in Journal Automated Software Engineering, 10(2), 2003. http://swtv.kaist.ac.kr/courses/cs750b-sw-model-checking-fall-06/ase00FinalJournal.pdf
- Tinelli: SMT-based model checking, in Formal Techniques Summer School, 2011. http://homepage.cs.uiowa.edu/~tinelli/talks/FT-11.pdf
- Susanne Graf and Hassein Saidi. "Construction of abstract state graphs with PVS." In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.
- Robert Floyd. "Assigning Meanings to Programs," in Proceedings of Symposium on Applied Mathematics, Vol. 19, J.T. Schwartz (Ed.), A.M.S., 1967, pp. 19-32.
- Formal Methods Wiki http://formalmethods.wikia.com/wiki/Formal_methods
The material (slides, literature, exercises) is provided in the TU Dortmund Moodle. Registration in LSF is mandatory and automatically perfoms enrolment in the Moodle.
Note on the language
The literature for the proseminar will be in English only. Presentations and papers may be in English or German.