The division pursues research and education within the broad field of Formal Methods. Formal Methods are a collection of notations, techniques and methods for describing and analyzing systems. These notations, techniques and methods are formal, meaning that they are based on mathematical theories like logic, automata or graph theory.
More concretely, our division performs research on the development and use of formal specification languages and verification approaches for different applications, including low- and high-level software, and (legal) contract analysis. Specification languages include classical and modal logics, and our verification techniques comprise model checking, automated reasoning, interactive theorem proving, static and runtime verification, and testing.
Our research group has a weekly recurring meeting in which people pitch their latest research ideas, ranging from a half-baked research idea to a dry-run before actual conference talk. We also welcome the visiting scholars to present their research works.
See our Google calendar for the latest update of our weekly meetings
You can sign up with our FM mailing list where activities are announced
Selected Research Projects
|PolUser||Rich User-Controlled Privacy Policies|
|AutoProof||An auto-active verifier for object-oriented programs written in the Eiffel programming language.|
|AutoFix||a tool for the automated repair of bugs in programs equipped with simple contracts (pre- and postconditions).|
|Hipster||Inductive theorem prover and theory exploraiton system for Isabelle/HOL.|
|QuickSpec||A theory exploration system.|
|TIP & TIP-tools||TIP is a language based on SMT-LIB for expressing problems for inductive theorem provers, as well as recursive datatypes and functions. TIP-tools is a collection of tools for translating and pretty printing TIP into and from various other formats such as SMT-LIB, TPTP and others.|
|KeY||KeY lets you specify the desired behavior of your program in the well-known specification language JML, and helps you proving that your programs conforms to its specification. That way, you did not only show that your program behaves as expected for some set of test values - you proved that it works correctly for all possible values! Go beyond testing - start proving!|
|CakeML is a functional programming language with a proven-correct compiler and runtime system.|
See this page for all available master’s thesis project proposals.
Formal Methods in Software Development In this course, you can acquire skills in two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. One is SPIN, a model checker for asynchronous processes. The other is KeY, a deductive verifier for Java software. The course builds on skills in first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software. This course is new, and will first be given in September/October 2017. For more information, see the predecessor course.