For background information on the topic as a whole, scroll to the end of this page.
Available Project Proposals
If you are interested in the general topic of Software Reliability, or if you have your own project idea related to the topic, please contact us directly. Alternatively, you can also work on one of the following concrete project proposals:
- Automatic contract generation for VerCors (Marieke Huisman, Alexander Stekelenburg)
Supervisor: Marieke Huisman and Alexander Stekelenburg
Recently, a plug-in for the Frama-C software analysis platform was released which infers ACSL contracts and loop invariants for C functions. More information about this plug-in can be found here:
- https://github.com/rse-verification/saida
- https://link.springer.com/chapter/10.1007/978-3-031-55608-1_13 (not available for free)
Saida's contract inference is built on the TriCera verification about which more information can be found here:
At the FMT group in Twente, we are developing the VerCors verifier for deductive verification of concurrent software, see https://vercors.ewi.utwente.nl/. One of the bottlenecks for deductive verification is writing specifications. Therefore, we would like to investigate if these automatic inference techniques could be used to reduce the annotation burden in VerCors.
The suggested steps for this research project would be:
- understand the class of programs for which Saida/TriCera's contract inference can be used
- identify examples that have been verified with VerCors which fit in this class of programs
- investigate whether the generated contract can be used to verify the programs with VerCors
- investigate whether it would be useful and feasible to integrate these automatic inference techniques with VerCors
- An Automated SystemC-to-C Transformation for Deductive Verification with Frama-C (Marieke Huisman, Philip Tasche)
(Supervisor: Marieke Huisman, Philip Tasche)
Embedded control systems are ubiquitous in modern life, including in safety-critical areas such as powerplants, motor vehicles or medical systems. As such, it is crucial to ensure their correct working. Furthermore, it is desirable to make such effort as early in the development process as possible, since an error caught early on costs much less to remedy than an error discovered later in the process. Therefore, it is desirable to verify correctness already at the design stage, when the program is written in a design language like SystemC.An effective technique for ensuring program correctness is deductive verification, which formally proves that a program complies with its specifications. However, tool support for deductive verification of SystemC is still rudimentary.
Your goal in this project is to change this by developing and implementing a transformation from SystemC to sequential C to allow for verification with the Frama-C verifier. To this end, you will extend previous work in the direction of such an automated transformation. You will become familiar with SystemC, Frama-C, deductive verification and language transformation.
Required steps for this project are:
- understand the semantics of SystemC
- understand the challenges in encoding SystemC in C such that it is useable by Frama-C and previous approaches dealing with this
- apply your findings to design a transformation
- implement your transformation
Some supporting resources:
- Documentation for Frama-C and the WP plugin for deductive verification
- A previous Bachelor thesis exploring the challenges is available upon request
- Paper on a transformation from SystemC to VerCors: DOI 10.1007/978-3-031-77382-2_23
- A Comparison of Frama-C and VerCors for the Deductive Verification of an Anti-lock Braking System (Marieke Huisman, Philip Tasche)
(Supervisors: Marieke Huisman, Philip Tasche)
Deductive verifiers - tools that can prove a program's correctness by means of logical deduction - differ in capabilities and limitations based on their underlying logics. What one verifier can prove without trouble, another might only be able to prove with a long verification time, by using a manual workaround, or not at all. The choice of verification tool is, therefore, an important question for any formal program verification approach.In the SAVES project, we are working on deductively verifying embedded systems written in the hardware/software co-design language SystemC. To this end, we have developed VeSUV, a verification tool based on the VerCors concurrency verifier, as well as general techniques for SystemC verification. However, while SystemC is technically concurrent, it only ever executes a single process at a time. This poses the interesting question whether this verification can also be done with a sequential verifier such as Frama-C, and whether the strengths of Frama-C outweigh the additional effort of encoding SystemC's concurrent processes in a sequential format.
Your goal in this project is to evaluate both VerCors and Frama-C on a case study of an anti-lock braking system (ABS) modelled in SystemC, and to conclude which is better suited for our purposes. You will become familiar with SystemC, Frama-C and VerCors.
You should have some prior experience with deductive verification.
The following steps are necessary for this project:
- understand deductive verification techniques for embedded systems
- familiarize yourself with SystemC, Frama-C and VerCors based on the provided materials
- verify some properties with Frama-C and VerCors
- evaluate benefits and weaknesses of each for SystemC verification
Some supporting resources:
- VerCors documentation
- Frama-C documentation
- VeSUV paper: DOI 10.1007/978-3-031-77382-2_23
- A Bachelor thesis on SystemC verification with Frama-C is available upon request
- A library for atomic operations in VerCors (Marieke Huisman)
Supervisor: Marieke Huisman
Many concurrent programs use atomic operations for efficiency reasons. In order to verify such programs, we need to provide formalisations of the atomic operations. We have several papers that describe suitable formalisations for atomic operations, but we lack a standard library that we can load if we wish to verify a new algorithm using atomic operations.
The goal of this project is to develop such a library. You will be expected to take the following steps:- study the papers that provide verification examples using atomic operations
- from these papers, distil one or more suitable formalisations of atomic operations
- provide these formalisations as standard libraries that can be reused in VerCors
- if time permits, provide a formal argument why the library specification is sound
- Find my invariant: Automatically infer Loop Specifications in Embedded Systems (Marieke Huisman, Philip Tasche)
Supervisors: Marieke Huisman, Philip Tasche
Embedded systems are used in a wide variety of appliances, including cars, planes or medical instruments. Many application areas are safety-critical, which makes it crucial to formally establish that these systems behave correctly. One tool to prove this correctness is VeSUV. This tool automatically encodes an embedded system modelled in the design language SystemC into the VerCors verifier for its deductive verification.The automated encoding allows the user to prove functional and safety properties about the system in question. However, the verification process is not fully automated, leaving the user to manually adjust loop invariants and function contracts to achieve the desired result.
The goal of this thesis project is to investigate ways to further automate the invariant generation process and thereby make verification easier. You will become familiar with VerCors, deductive verification, invariant generation and VeSUV.
The following steps are necessary for this project:
- understand deductive verification with VerCors, including contracts and loop invariants
- investigate specification inference techniques
- apply these techniques to the specific problems encountered in embedded system verification
- implement your approach in the VeSUV tool
Some supporting resources:
- VeSUV paper: DOI 10.1007/978-3-031-77382-2_23
- VerCors Wiki
- Carlo Alberto Furia and Bertrand Meyer: Inferring Loop Invariants Using Postconditions. In: Fields of Logic and Computation. LNCS 6300. Springer 2010. (https://doi.org/10.1007/978-3-642-15025-8_15)
- Good relationships are important! Adding VerCors support for relational verification (Marieke Huisman, Robert Mensing)
Supervisors: Marieke Huisman, Robert Mensing
Traditionally, program verification focuses on proving functional properties of a program: if a program is executed, it will compute a certain value, or reach a certain state. Recently, several people have developed techniques for relational verification, which establishes a relationship between the execution of two different programs (or even of the program with itself) [1, 2, 3, 4].Relational verification has been used for example for information flow properties [1, 7], slicing [2] and regression verification [6]. The VerCors verifier that we are developing in the Formal Methods and Tools group at the University of Twente currently does not support relational verification, while Viper (the verifier underlying VerCors) does support this [7, 8]. In this assignment, we ask you to study the different approaches to relational verification, and to see how we can extend the VerCors verifier to support relational verification.
Typical steps in the project would be:
- understand existing approaches to relational verification in the literature
- identify which approach would fit well with VerCors
- propose a design to extend VerCors with relational verification support
- implement the support
Some relevant literature
[1] Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. CSFW 2004: 100-114
[2] Gilles Barthe, Juan Manuel Crespo, César Kunz: Relational Verification Using Product Programs. FM 2011: 200-214
[3] Ádám Darvas, Reiner Hähnle, David Sands: A Theorem Proving Approach to Analysis of Secure Information Flow. SPC 2005: 193-209
[4] Moritz Kiefer, Vladimir Klebanov, Mattias Ulbrich: Relational Program Reasoning Using Compiler IR. VSTTE 2016: 149-165
[5] Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich: SemSlice: Exploiting Relational Verification for Automatic Program Slicing. IFM 2017: 312-319
[6] Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl: Regression Verification for Programmable Logic Controller Software. ICFEM 2015: 234-251
[7] Marco Eilers, Peter Müller, Samuel Hitz: Modular Product Programs. ESOP 2018: 502-529
[8] Marco Eilers, Severin Meier, Peter Müller: Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. CAV (1) 2021: 718-741 - Macros for verification (Marieke Huisman, Alexander Stekelenburg)
Supervisor: Marieke Huisman and Alexander Stekelenburg
The C and C++ languages (and others) use a preprocessor to split up a codebase into multiple files and enable the use of macros to make the language more ergonomic. Many C libraries use macros and these libraries would be cumbersome to use without these macros.
For software verification we write the specifications in comments, but these comments are ignored by the preprocessor. This means that macros will not be expanded inside specifications which makes writing specifications cumbersome compared to writing code. Additionally, preprocessors only include line information in their output which makes it impossible to find the correct column to point to if an error occurs in a macro expansion.
We would like to investigate if and to what degree improving macro support would allow us to support verifying C code that uses libraries. Additionally, since macros can be used to generate repetitive code they may also be useful for generating repetitive specifications.
The goal of this project is to determine how macros can aid verification, and to design and implement a C/C++ preprocessor to allow us to use macros in more cases. The preprocessor should be able to expand macros inside and outside of comments, and should preserve line and column information such that errors can be precisely located in error messages.
There are multiple approaches we can take, which of these is optimal depends on how macros are used in real C/C++ projects and how we would like to use them in annotations. Both the Frama-C and VeriFast verifiers use a custom preprocessor for this purpose, but the implementation is too closely entangled with these verifiers to be re-used by other tools.
We would like to use such a preprocessor for the C and C++ frontend of the VerCors deductive verifier that we develop here at the FMT group in Twente. You can find out more about VerCors here: https://vercors.ewi.utwente.nl.
- Prove your (functional) Algorithm in Isabelle/HOL (Peter Lammich)
Supervisors: Peter Lammich
Interactive Theorem Provers (ITPs) provide a way to develop computer checked (mathematical) proofs. In particular, they can be used to prove programs correct. In this project, you will learn to use an ITP, and apply it to prove correct a functional program or data structure of your choice (agreed on with the supervisor). - Smoke testing for VerCors (Marieke Huisman, Alexander Stekelenburg)
Supervisor: Marieke Huisman and Alexander Stekelenburg
Smoke tests are automatic checks that aim to find inconsistent specifications and other things that might be unintended errors such as dead code. Since writing specifications for verifying the correctness of programs can be difficult it is useful to automatically discover mistakes.
The deductive verifier that we develop here at the FMT group in Twente is called VerCors. You can find out more about VerCors here: https://vercors.ewi.utwente.nl/. It already does a basic form of smoke tests, namely it checks whether the precondition of a method is satisfiable. (i.e. it is not inconsistent with itself)
However, recently a paper describing the implementation of different kinds of smoke test for Frama-C's deductive verification plugin was published. We would like VerCors to also do these other kinds of smoke tests. The paper can be found here: https://link.springer.com/chapter/10.1007/978-3-031-72044-4_4
The goal of this research project is to figure out which kinds of smoke test we should implement in VerCors, how these can be implemented, and how effective these tests are.
- Translating specifications for deductive verifiers (Marieke Huisman, Alexander Stekelenburg)
Supervisor: Marieke Huisman, Alexander Stekelenburg
Deductive verifiers can be used to prove correctness of a program. To determine whether a program is correct, the user needs to give a program and its specification to the verifier. These specifications are typically written in a specification language, often inspired by predicate logic. However, while very similar, specification languages for different verifiers often have slightly different semantics, due to which it is difficult to reuse specifications from other verifiers.We have developed the Specification Translator, a tool to translate specifications between several deductive verifiers for Java programs. It currently supports Krakatoa, OpenJML and VerCors specifications. As a result, we are now able to reuse specifications between these three verifiers.
In this project, we ask you to add support for another deductive verifier to the Specification Translator. An interesting candidate for this is KeY. You will have to study the differences in semantics of the specification languages, and see how support for KeY's specification language can be added to the Specification Translator.
You will be expected to take the following steps:
- Understand KeY's specification language
- Identify differences between the semantics of KeY's specification language and the languages currently supported
- Implement support for KeY's specification language in the Specification Translator
- Using LLMs to generate specifications for VerCors (Marieke Huisman)
Supervisor: Marieke Huisman
LLMs have become popular for various uses and in academia, the usability of LLMs (large language models) for many use cases is researched. One of these uses is the automatic generation of specifications for deductive verifiers. Recently, a paper was published that uses LLMs to generate formal specifications for a given program (link below).
Here at UTwente, the FMT group develops a deductive verification tool called VerCors. For more info see https://vercors.ewi.utwente.nl/.
The goal of this research would be to see how applicable the approach from the paper is to the VerCors deductive verifier.
The paper: Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification (https://link.springer.com/chapter/10.1007/978-3-031-75387-9_15)
- VerCors support for quantitative separation logic (Marieke Huisman)
Supervisor: Marieke Huisman
Recently, a quantitative separation logic to reason about probabilistic pointer programs has been proposed. In Twente we are developing the VerCors program verifier, which uses separation logic to reason about (concurrent) programs. In this project, we would like to investigate how we could adapt the setup of the VerCors verifier such that it could support this quantitative separation logic.
The following steps would be necessary:- understand the quantitative separation logic
- understand the VerCors architecture
- investigate how to adapt the VerCors architecture such that it could support quantitative separation logic
- implement the necessary changes
Contact



Background
Software is everywhere! Therefore, our society heavily depends on the correctness and reliability of this software: we need techniques to show that software always behaves in the way that we expect, e.g. it will not crash, it computes the results that we expect, it does not have bugs and it does not violate the security or privacy of its users.
To guarantee the correctness and reliability of software, within the FMT group, we develop various verification techniques to reason about software.
First of all, we develop the VerCors program verifier, a tool set to verify concurrent and parallel programs: the user specifies the desired behaviour in terms of pre- and postconditions (and possible auxiliary annotations), and the tool then tries to automatically check whether the program respects the specification. The VerCors verifier can reason about (concurrent and parallel) programs written in Java, (a subset of) C, and OpenCL.
Second, we also develop the Refinement Framework within the Isabelle interactive theorem prover. Interactive theorem provers allow users to develop proofs (eg. that a program is correct) that are checked by the computer to rule out errors. The Isabelle Refinement Framework allows one to first verify an abstract version of a program, and then refine it, in several correctness preserving steps, to a concrete efficiently executable program. The Isabelle Refinement Framework has been used for various (sequential) algorithms, which eventually were refined into Standard ML or LLVM programs.
We offer student research projects related to program verification. These projects can be on different topics:
- verification of non-trivial case studies,
- development of new verification technology, for example defining semantics and verification techniques for a new language feature, or
- improvement of the tool support.
Prerequisites
- Programming experience
- Familiarity with specifications in first-order logic
Related Modules
- Software Systems (pre- and postcondition specifications)
- Discrete Structures and Algorithms (automata and graph algorithms, semantics)
- Programming Paradigms (concurrent programming, functional programming)