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)

## 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:

- Prove your (functional) Algorithm in Isabelle/HOL
*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). - A library for atomic operations in VerCors
*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

- Bounded numbers support for VerCors
*Supervisors: Marieke Huisman, Ömer Şakar*

The VerCors program verifier can reason about programs with integers. When reasoning about these integers, we interpret them as mathematical integers. However, in real programs these integers are machine integers or bounded integers. Besides integers, VerCors currently does not support reasoning about bytes, shorts and similar.

In this project, we would like to investigate how we can add support for bounded numbers (e.g. integers, bytes, shorts and similar):

The following steps would be necessary:- understand how bounded numbers are encoded
- understand how different modes for reasoning (e.g. bounded, mathematic) can be supported
- understand the VerCors architecture
- investigate how to add bounded numbers into VerCors
- implement the necessary changes

- VerCors support for quantitative separation logic
*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

- Good relationships are important! Adding VerCors support for relational verification
*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 - Improving the rewrite system for expressions of VerCors
*Supervisors: Marieke Huisman, Ömer Şakar*

The VerCors program verifier transforms input programs step-by-step into its backend Viper and in turn to Z3, the SMT solver. One of these transformations is rewriting expressions to make it easier for Z3 to verify them.

The current rewrite system allows for rewrite rules that are purely syntactical. This means that an expression is rewritten only if it matches the rewrite rule exactly. This approach lacks support for more complex and expressive rewrite rules.

In this project, we would like to investigate how we can improve the rewrite system.

The following steps would be necessary:- understand the rewrite system
- understand the VerCors architecture
- investigate how we can adapt the current rewrite system to support more complex rewrite rules
- implement the necessary changes

- Find my invariant: Automatically infer Loop Specifications in Embedded Systems
*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:

- A paper on VeSUV is available upon request
- 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)

- Translating specifications for deductive verifiers
*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

- A Comparison of Frama-C and VerCors for the Deductive Verification of an Anti-lock Braking System
*(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:

- An Automated SystemC-to-C Transformation for Deductive Verification with Frama-C
*(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:

- Automatic contract generation for VerCors
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

The project is supervised by Prof. Dr. Marieke Huisman and Alexander Stekelenburg MSc.