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 Courses

Available Project Proposals

If you are interested in the general topic of Software Reliability, or if 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


    Supervisor: 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).

  • Verify an Imperative Algorithm in Isabelle-LLVM


    Supervisor: Peter Lammich
    Isabelle-LLVM is a verification framework for LLVM IR based on separation logic and the interactive theorem prover Isabelle HOL. In this project, you will verify some imperative (sequential) algorithm or data structure using Isabelle-LLVM. Prerequisite: Interactive Theorem Proving course. 

  • Deductive verification for LLVM-IR


    Supervisors: Marieke Huisman, Ömer Şakar
    LLVM IR is Static Single Assignment (SSA) language that aims to be an intermediate representation language. It is light-weight and close to assembly allowing many different languages (e.g. C and SYCL) to be compiled to LLVM and to be ran on differences devices (e.g. CPUs and GPUs), making the verification for this language very intersting.
    Verification of software aims to prove different properties (e.g. functional correctness and data-race freedom) over the source code. There are different approaches to verifying code such as model checking and deductive verification and there are tools supporting these approaches (see references). Within the FMT group, we are developing a deductive verification tool VerCors for the verification of concurrent and distributed software. It uses permission-based separation logic to reason about software, specifically concurrent software.
    In this project, you are asked to take a look at how LLVM code can be verified using permission-based separation logic. Concretely, we expect you to take the following steps:

  • Case study: verification of a distributed lock


    Supervisors: Marieke Huisman, Stefan Blom, Bob Rubbens
    BetterBe uses a distributed lock to synchronize JVM processes. The distributed lock is implemented in Java and uses a shared database. The code is known to work in practice, but the question remains: is this a correct implementation of a read/write lock?
    VerCors is a deductive verifier developed at the FMT group. It can verify memory safety and functional correctness of Java, C, and GPGPU programs written in OpenCL. VerCors allows the user to specify pre- and post-conditions in the style of JML, extended with separation logic. This allows the user to annotate the code with read/write access patterns to data. VerCors can analyze these annotations and determine whether the code complies.
    For this assignment, the student will formally verify the correctness of the distributed lock implementation with VerCors. To accomplish this task, several subtasks must be done:

    • Understand the distributed lock implementation
    • Verify memory safety of the lock implementation with VerCors
    • Model the locking protocol, and verify adherence to the protocol, with VerCors Models
    • Analyze correctness, fairness, and progress of the locking protocol in mCRL2

      These subtasks are hard problems, and might require abstraction of the source code, or possibly modification or extension of the VerCors verifier. The project will partially be supervised by BetterBe staff. The distributed lock is implemented in Java, and the source is available for inspection.

      Supporting material
    • BetterBe homepage
    • VerCors homepage
    • VerCors GitHub repository
  • Case study: round-robin throttled blocking queue


    Supervisors: Marieke Huisman, Stefan Blom, Bob Rubbens
    BetterBe uses a throttled blocking queue to spread out work over time. This prevents overloading the external servers. Initial versions of this throttled blocking queue have shown problematic behaviour, which caused unfairness and starvation of processes. This has since been fixed. However, without formal analysis, we cannot be sure that the problematic behaviour is absent.
    VerCors is a deductive verifier developed at the FMT group. It can verify memory safety and functional correctness of Java, C, and GPGPU programs written in OpenCL. VerCors allows the user to specify pre- and post-conditions in the style of JML, extended with separation logic. This allows the user to annotate the code with read/write access patterns to data. VerCors can analyze these annotations and determine whether the code complies.
    For this assignment, the student will formally verify the correctness and fairness of the throttled blocking queue implementation with VerCors. To accomplish this task, several subtasks must be done:

    • Understand the throttled blocking queue implementation
    • Understand the bug and how it was fixed
    • Verify memory safety and functional correctness of the implementation with VerCors
    • Detect the bug with VerCors
    • Define in what sense the throttled blocking queue is fair
    • Formally verify fairness of the implementation using VerCors, VerCors models, and/or mCRL2.

      These subtasks are hard problems, and might require abstraction of the source code, or possibly modification or extension of the VerCors verifier. The throttled blocking queue is implemented in Java, and both versions of the source (before and after the problematic behaviour was fixed) are available for inspection. The project will partially be supervised by BetterBe staff.

      Supporting material
    • BetterBe homepage
    • VerCors homepage
    • VerCors GitHub repository
  • Formal Verification of Efficient Data Structures for Web Services to Automotive Lease Companies


    Supervisors: Stefan Blom, Marieke Huisman, Lukas Armborst
    BetterBe is a company, based in Enschede, that provides webservices to automotive lease companies, in particular, to calculate the price of a particular lease car.
    Calculating this price is more complex than one may think, because of the large number of intricate dependencies between the various options. For instance: if you opt for a sports package, you cannot choose certain radios (reason: the leather steering wheel coat does not have the right holes for the radio buttons). There are hundreds of such dependency rules. Therefore, figuring out if a certain set of option is feasible, and determine its price, is non-trivial.
    Two aspects of the price calculation are very important: speed and correctness.
    Speed of this price calculation is of utmost importance: every click in a car leasing website triggers a lease calculation, which must be fast, for users to have a pleasant user experience. But even more important than speed is correctness. Users may not lease cars when the calculated prices are too high, and leasing companies may make huge losses when the calculated prices are too low.
    To achieve speed of calculation, BetterBe builds its software using a number of efficient basic data structures, of which a red-black tree and a multi-hash-table are the most important. Correctness of the implementation of these basic data structures is thus very important, not only to obtain correct price calculations, but also to obtain them as fast as possible: performance may seriously suffer when red-black trees lose their balance.
    Formal verification using static analysis techniques is seen as possible solution that may give BetterBe rigorous proof of correctness, or clear indication of errors.
    In practice, this means (1) to formulate invariants to which the data structures have to comply, and (2) to show that the data structures do not invalidate these invariants. In an earlier MSc project and a paper, a standard red-black tree data structure has been proven (functionally) correct, as a first step in this project. The current project is about taking the next step, and adapting the standard data structure towards the specific data structure used at BetterBe. 

  • Verification of distributed algorithms


    Supervisor: Marieke Huisman
    Within the FMT group, we are developing the VerCors tool set for the verification of concurrent and distributed software. We have developed an abstraction technique that can be used to reason about the behaviour of a concurrent or distributed program. in earlier work, we have shown that this approach is suitable to reason about a distributed leader election protocol.
    In this project, you are asked to investigate the suitability of this approach for other distributed algorithms, by verifying multiple classical distributed algorithms using our abstract model approach. Ultimately, we would like to understand how we can further automate this process, for example by automatically identifying the abstract models. Concretely, we expect you to take the following steps:

    • understand program verification and abstract models as supported by VerCors
    • identify classical algorithms that can be verified using this approach
    • provide abstract models for these classical algorithms
    • prove that the algorithm implements the abstract model for these examples
    • develop techniques to further automate this process 
  • Verification of (parallel) model checking algorithms


    Supervisor: Marieke Huisman
    Within the FMT group, we are developing the VerCors tool set for the verification of concurrent and distributed software. To demonstrate the usability of our verification technique, we have recently used it to verify the correctness of a parallel nested depth first search algorithm, which can be used for reachability analysis in model checking.
    In this project, you are asked to investigate how to further improve the use the VerCors tool set for the verification of other (parallel) graph algorithms. Possible points for improvement are: 

    • developing a library of suitable, reusable graph properties,
    • automatically generating graph-related annotations for the algorithm,
    • identifying the best way to represent graphs,
    • refining the verification of a high-level algorithm into a verified, efficient implementation.

      During this project you will take the following steps:
    • understand program verification using VerCors
    • identify a suitable (parallel) model checking algorithm
    • formalise the desired correctness properties
    • prove correctness of the high-level algorithm w.r.t. the desired correctness properties using the VerCors tool set
    • investigate how to turn the verification into reusable results 
  • Formal modelling and verification for the Maeslantkering

    supervisor: Marieke Huisman
    The Maeslantkering is the biggest water defense work in the Netherlands. It is larger than the Eiffeltower. It protects the industrial and harbour area of Rotterdam. There are two locomotives to close the two doors that prevent influx of water into the river Rhine at high tide. The software in these locomotives needs to be replaced, as the PLC's inside them are end of life. Rijkswaterstaat requested whether it is possible to formally model the new software for the locomotive, and prove it correct to guarantee that the new locomotive works flawlessly, at any time, especially in those times of need. They are looking for a master student that is willing to try different modelling and verification techniques, to see which one would be suitable for this application.

  • Automated security verification of code for embedded devices


    Supervisors: Marieke Huisman, Roeland Krak
    One of the problems with automated code verification for embedded devices is the presence of many context-specifics that influence execution. For example, hardware architecture, OS behaviour and software separations all come into play when verifying embedded code. The goal of this project is to contribute to automated verification techniques so they can take execution context into account.
    Specifically, the project focuses on development of a methodology for automated identification of context-specific vulnerabilities in C code. To ease development of the solution, it can use a prototype front-end developed by Riscure to interact with the user and code in an organized way.
    We expect the project to contain the following elements:

    • Study of the problem domain
    • Development and implementation of a proposed solution
    • Validation of the solution

      We are looking for a motivated student with a technical interest in security and formal verification to join our Delft office as an intern to perform this project. For more information and applications please contact Karolina Mrozek (mrozek@riscure.com). 
  • VerCors support for SecCSL

    Supervisors: Marieke Huisman, Sophie Lathouwers
    Ernst and Murray[1] recently proposed SecCSL, a concurrent separation logic for proving information flow security properties. In the FMT group we have developed the VerCors program verifier, which uses concurrent separation logic to reason about the correctness of programs. In this project, we want to investigate how we could adapt the VerCors verifier to support SecCSL.
    The following steps would be necessary:

    • Understand SecCSL
    • Understand the VerCors architecture
    • Investigate how to adapt VerCors to Support SecCSL
    • Implement the necessary changes

      References
    • [1] "SecCSL: Security Concurrent Separation Logic" by G. Ernst and T. Murray (CAV 2019) https://doi.org/10.1007/978-3-030-25543-5_13
  • Automatic annotation generation for barriers on GPUs: From GPUVerify to VerCors


    Supervisors: Marieke Huisman, Ömer Sakar
    With increasing capabilities of GPUs, many sequential programs migrate into GPUs to gain more performance, but verifying the correctness of GPU programs is still challenging. The tool VerCors is developed in our group to verify concurrent programs. It accepts various input languages (Java, OpenMP, OpenCL, PVL), along with annotations, and checks properties like data race freedom and functional correctness of the program. In the case of GPU programs, these annotations are as pre/postconditions in the kernels and barriers. Barriers are mechanisms in GPU programs to synchronize the execution of threads in one block.
    There is a another tool, GPUVerify, developed at Imperial College London, to verify only data race freedom of GPU programs. The advantage of this tool, compared to VerCors, is that they can generate annotations automatically. Since they generate annotations for barriers, we would like to investigate how we can use it to generate annotations for barriers in VerCors.
    Tasks:

    • Understand how VerCors and GPUVerify work.
    • Understand how annotations are generated for barriers in GPUVerify.
    • Discover how VerCors can benefit from step 2 to generate annotations for barriers.
    • Implement step 3 in the VerCors toolset. 
  • Empirical Study on Design by Contract Teaching


    Supervisors: Raúl Monti, Marieke Huisman
    We propose to carry out an empirical study at Dutch schools to determine the effectiveness and limitations of our approach to teach Design by Contract and Software Verification to the students from the last years of secondary school.
    We have the description of our approach and a preliminary plan supported by an extension to the Snap! language [1,2,3] that can be found at [4]. The approach should be reviewed and the teaching plan should be elaborated. Also, the experiment has to be set up and the guidelines for its result analysis have to be established. We need to search for suitable institutions where to carry out the study. Finally we need to carry out the study, finding a way to overcome the limitations of the pandemic situation, if any remain by the time the research is realised.
    References:
    [1] https://snap.berkeley.edu/
    [2] https://snap.berkeley.edu/snap/snap.html
    [3] https://bjc.edc.org/
    [4] https://git.snt.utwente.nl/montire/verifiedsnap 

  • Verification of concurrent tree bitmaps


    Supervisors: Marieke Huisman, Lukas Armborst
    This project is in cooperation with the company NLnet Labs. At NLnet Labs we build software tools to analyse the state of the Internet routing infrastructure in near real-time. We know the position and destination of airplanes in the sky at any time, but which routes our Internet traffic takes is a very challenging problem that we want to tackle. To this end we are researching and building an engine that at its core has a data-structure that will be able to store and retrieve this data (centred around IPv4/v6 prefixes). The most important properties of the desired solution are that the data structure is time and space efficient, which traditionally is always a trade-off between the two.
    Currently we have implemented this data-structure as a treebitmap, you can read more about the considerations that led to this choice here. An explanatory implementation of this data-structure, as well as some implementations using other underlying data-structures, can be found here.
    We are now considering a production implementation that can be used in multi-threaded environments, with multiple writers and readers using a single data-structure concurrently. We are comparing two main directions to approach this problem:

    • A single writer on a single thread with a queuing mechanism and single-threaded readers (one thread per reader) concurrently accessing the data-structure. In this case there's only a need for concurrent read access. This would be the baseline implementation to compare other implementations to, in order to gauge the costs versus the benefits of other solutions in terms of performance and safety guarantees.
    • Multiple Writers and multiple readers (MPMC). This will need both concurrent write and read access.
    • For concurrent access we will compare both lock and lock-free data-structures, although we are biased towards lock-free ones (using atomics), since these are not prone to dead-locks and should perform better under contention than lock-based data-structures. Ideally speaking we would like to implement a wait-free data-structure, but that might prove to be over-engineering.
      Note that we may also end up with a mixture of both single-writer and multiple-writer data-structures, due to the specific properties of BGP data streams. BGP data streams have episodes of bursts of concurrent writes (the convergence period on startup or after `route-refresh` commands) and episodes of low-intensity writes from many sources and medium-intensity reads from many sources. The result of mixing both solution directions may very well mean that we will have to come up with a tree-merging strategy.
      Another issue that will need to be considered, is memory reclamation. We don't think the removal of IP prefixes (and thus removal of nodes in our tree) will play a big role and we will be able to get away with stop-the-world tree pruning at strategic moments in time (comparable to the way Postgresql does this). If it turns out this would not be a good approach after all, we need to consider strategies that handle the ABA problem, like epoch-based memory reclamation.
      Project: Verification could hopefully make a comparison between the baseline implementation and the lock-free MPC one, and give us guarantees about our implementation indeed being dead-lock free, and maybe even starvation-free, as well as guarantees around avoiding the ABA problem.
  • Verification of private machine learning algorithms

    Supervisors: Petra van den Bos, Milan Lopuhaä-Zwakenberg

    Differential Privacy (DP) is a metric to measure the privacy leakage of an algorithm handling sensitive data. Because of its strong privacy guarantees it is widely used in both industry and academia. An important application is private classifier training, where a data classifier must be created based on training data, without leaking too much information about the training data itself. In this project, the student investigates the formal verification of DP algorithms. More concretely:

    • Implement DP classifiers into formal verification tools to verify their privacy;
    • Study the difference, in implementation and verification guarantees, of static vs dynamic verification;
    • See whether these tools have the functionality to verify a range of DP classifiers.
  • Verifying 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. The result should be 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
    • develop an automatic procedure to translate, and ideally also prove, new rewrite rules

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

Contact