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.


Formal Methods for Software Development


Link to Page

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:

Testing, Debugging, and Verification


Link to Page

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:

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.

Other courses supported by FM division

Principles of Concurrent Programming


Link to Page

Compiler Construction


Link to Page