Software Reliability

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:

Prerequisites

Related Modules

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 
  • Improved support for non-linear arithmetic

    Supervisors: Marieke Huisman, Bob Rubbens
    Program verification with VerCors relies on SMT solvers such as Z3 to compute whether or not formulas hold. SMT solvers are good at solving Boolean and simple arithmetic. However, when non-linear arithmetic is used, such as multiplication or modulo, proving programs correct becomes difficult. Furthermore, support for non-linear arithmetic is often not directly usable.
    The goal of this project is to determine the limits of and tuning needed to use the non-linear arithmetic support in SMT solvers with VerCors.
    This is done through the following steps:

    • Study papers documenting support for non-linear arithmetic in SMT solvers
    • Document the kinds of non-linear arithmetic that are supported and their limits
    • Find, and possibly design, examples to test the non-linear capabilities of SMT solvers
    • Categorize and benchmark the different flags, options, and their values, for tuning non-linear arithmetic solving.
  • 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 
  • Termination checking support in VerCors

    Supervisors: Marieke Huisman, Petra van den Bos
    Termination of a program is usually a desired property, but sometimes the programmer unintentionally violates this property. For example, if the programmer wrote a non-terminating loop, or used a function call resulting in non-terminating recursion. In this project you will study program termination and implement verification support in the tool VerCors. You will focus on proving termination of loops. Note: In principle it is well-known how to reason about termination, but the challenge of this project is to incorporate this well-known technique into the VerCors verifier.
    You will be expected to take the following steps:

    • Study papers about verification of loop termination.
    • Write an example program with loop termination specifications.
    • Understand the VerCors architecture.
    • Investigate how to adapt the VerCors architecture such that it supports loop termination specifications.
    • 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, Lukas Armborst
    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 
  • Verifying the correctness of VerCors rewrite rules

    Supervisors: Marieke Huisman, Lukas Armborst, Bob Rubbens
    The verification tool VerCors, developed here in the FMT group, transforms the annotated input program into something that the backend tools can check. As part of this transformation, some expressions are rewritten into equivalent ones. However, this equivalence is simply assumed, and not formally proven. This project aims to prove that equivalence, thus closing this gap in the formal proof chain.
    We propose to use the Coq interactive theorem prover for this, which has support for separation logic via the Iris plugin. So a significant part of this project is to determine how VerCors' rewrite rules should be expressed in Iris. Ideally, the result is a reusable procedure that can also be applied to new rewrite rules in the future, to facilitate a (semi-)automatic proof for them.
    The following steps would be necessary:

    • understand the VerCors rewrite rules
    • get familiar with Coq and Iris
    • translate the expressions from the VerCors rewrite rules to Iris expressions
    • prove those Iris expressions

    Familiarity with interactive theorem proving, or a strong interest in obtaining it, is highly beneficial.

  • An empirical study for teaching verification using Snap!

    Supervisors: Marieke Huisman, Raúl Monti
    Snap! [1] is a graphical programming language tailored to teaching programming at schools. Two previous projects in our group have been able to extend Snap! to include verification, with blocks that allow to define contracts that can be verified both dynamically [2] and statically via an encoding into the Boogie verifier [3]. Even though the graphical approach of Snap! has already been evaluated as an effective tool for teaching programming at initial levels of education, we still have no empirical study on the our approach of teaching verification with it.
    We propose that you design and undertake an empirical study to analyse how good our approach is for teaching verification via the Snap! extensions projects. We would like to know not only the quality of the approach but also what we can improve in our approach in order to maximize its impact in education.
    The COVID lock-down situation (ongoing by Spring 2021) suggests further challenges for an empirical evaluation of school students. We propose to define two approaches for it, one applicable inside a classroom in a normal teaching situation, and one that is also applicable in a lock-down situation where classrooms are closed and teaching is done virtually. It would be interesting to compare results of both types of evaluations.

    References

Contact