Education Program at FM
Master Thesis Projects
Our research group at Chalmers provides high quality FM-related courses as well as researh-oriented master thesis opportunities. If you are looking for FM-related master thesis topics, please take a look at here.
Courses
Formal Methods for Software Development
TDA294/DIT271
Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigor. The purpose is to construct, with high confidence, systems that behave according to their specification. The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool.
On the model checking side, the advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. Accordingly, we concentrate on the verification of safety properties. The lectures cover the following topics:
Theoretical foundations of model checking. Property languages and their usage. Performing automated verification with a software model checking tool. For the deductive verification side, we use KeY, an integrated tool for the formal specification and verification of Java programs. The tool, which is partly developed at Chalmers and Gothenburg University, supports formal specification in the Java Modeling Language (JML), and translation from JML into logic. An interactive theorem prover is used to formally verify statements about specifications and programs. The lectures cover the following topics:
- Java Modeling Language (JML)
- Formal Semantics of Systems
- Predicate Logic for Specification of Java Programs
- Translating JML into Dynamic Logic
- Verifying Proof Obligations
Testing, Debugging, and Verification
TDA567/DIT082
The course is about how to convince oneself that a program unit really does what it should. There are different methods for verifying programs that will be covered in this course:
- testing (which has the purpose of finding errors in a program in a systematic way)
- debugging (which has the purpose to systematically trace and eliminate an error)
- proving or formal verification (reasoning about the program in order to guarantee correctness).
Verifying a program only makes sense if we can precisely specify what the program is supposed to do. Many specifications are written in natural language which might lead to imprecision and misunderstandings. In the course you will learn how to use precise methods for specifying functional requirements. Such precise specifications will then be our basis for the verification of programs. But they will also be useful to automatize the generation of test cases.