Software and Computational Systems Lab

Software Verification Witnesses are a widely adopted tool to exchange information about tools centered on quality assurance, like fuzzers, model checkers, deductive verifiers, between many others. Currently only witnesses can only express a subset of what is required to present a complete violation or proof for all possible programs. Goal of this thesis would be to do an extension of the format and implement support for this extension in one of multiple directions. For example, for other program features like arrays and concurrency, for other programming languages like Java and Rust or for other specifications like memory safety.

When an automatic model checker finds a proof or a bug, it exports it as a witness. These outputs of the verification process can be independently validated by using a Validator. One of these validators is Metaval, which instruments the program using the information present in the witnesses. Goal of this Thesis is to reimplement Metaval for the new witness format 2.0.

When an automatic model checker finds a but, it reports it as constraints on the possible execution paths in form of a violation witness. These constraints are then used by a witness validator in order to replay the violation. The goal of this thesis is to make the restrictions on the state space available to all automatic verifiers by introducing them into the source code of the program.

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. Usually everything required to build a deductive verifier is inside an automatic verifier. The goal of this thesis is to create a deductive verifier out of the highly successful automatic verifier CPAchecker.

Automatic software verification tries to automatically proof that a program fulfills a specification without human input. On the other hand deductive verification requires manually writing annotations to proof the program correct. The goal of this thesis is to combine the strengths of both approaches by writing a tools which generates proof goals using information information provided by the user, but allow some of the information to be missing for it to be automatically verified by an automatic verifier.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. After having solved the transformed task, we want to transform the witness i.e. the information the verifier provided for the verdict of the program to a witness for the original program. The goal of the thesis is to implement such a transformation of witnesses.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. No-Datarace and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the No-Datarace property to the Reach-Safety property, which opens new options for No-Datarace analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves No-Datarace, implement the transformation in a tool and observe whether it is more efficient to solve No-Overflow using Reach-Safety analysis.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Memory-Safety and Reach-Safety property are both safety properties of the program with different atomic propositions. By instrumenting C programs, we can convert the Memory-Safety property to the Reach-Safety property, which opens new options for Memory-Safety analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to develop an idea of transformation C programs so that Reach-Safety analysis proves Memory-Safety, implement the transformation in a tool and observe whether it is more efficient to solve Memory-Safety using Reach-Safety analysis.

Algorithms for analysis of C programs are usually designed to verify a concrete class of properties of the C programs. Many of the properties of C programs that are checked by verifiers have a similar form. Thread-Liveness property is a liveness property, whereas Reach-Safety is a safety property. It is well-known that liveness can be transformed to safety. By instrumenting C programs, we can convert the Thread-Liveness property to the Reach-Safety property, which opens new options for Thread-Liveness analysis using algorithms that are used for Reach-safety tasks. The goal of the thesis is to implement the transformation in a tool and observe whether it is more efficient to solve Thread-Liveness using Reach-Safety analysis.

Due to the rising availability of distributed computational power distributing a verifier is of great interest. While distributing a single verifier is important, we consider how to use verifiers as building blocks in order to achieve distributed verification. Your goal would be to create a framework to make this possible, based upon some existing theory.

It has been shown that program transformations can improve the performance of verifiers. Compilers manage to produce highly optimized code which usually contains less instructions, loops and function calls. In this thesis your job will be to analyze what compiler optimizations improve verification tasks and generate a heuristic which optimization options should be used for what programs. A rudimentary framework to run experiments already exists.

K-Induktion is an analysis which uses candidate invariants to proof the safety of a program. These candidate invariants are currently obtained from a dataflow analysis inside CPAchecker. There are a lot of tools which produce different invariants for C-Programs, it would be interesting to see if they can help improve K-Induction.

CPAchecker is a very successfull tool for model checking. In particular it contains a lot of the components required to make use of it for checking data integrity. The goal of this thesis would be to implement a data integrity analysis in CPAchecker and evaluating it on a set of benchmarks.

CPAchecker is a very successfull tool for model checking. Currently it lacks support for different Hyperproperties, for example secure information flow. Goal of this thesis would be to add support for Hyperproperties to CPAchecker.

Finding good predicates is a key challenge for verifying programs using predicate analysis. Currently some heuristics and interpolation techniques are used to find new predicates. On the other hand machine learning techniques have been succesfull in determining invariants for programs. The goal of this thesis would be to use the information generated during the exploration of the state-space of a program to find good predicates/interpolants using machine learning techniques.

Deductive and Automatic Verifiers are two classes of verification methods to proof the safety of program. In this thesis the goal is to close the gap between them by transoforming an annotated program into proof goals and then using an automatic verifier to proof them. Building such a tool would be based upon a tool to treat Verifiers as SMT solvers which understand the intricacies of programming languages.

A verifier tries to proof that a property holds for a program. There are multiple properties a verifier can usually proof, for example Termination, Reachability, Memory Safety, etc.... Verifiers usually specialize on a couple of properties and optimize their algorithms for it. The goal of this thesis would be to implement a tool which does program transformation from any specification to any other and compare the performance of different verifiers on them.

It has been shown that program transformations can improve the performance of verifiers. Currently most approaches to program transformations change the code without using information collected during the verification process. The goal of this thesis is to improve upon this by developing some transformations on the source code of a program which make verification easier and incorporate information collected during the verification process.

Partial Order Reduction is a technique to reduce the state space of a concurrent program. The goal of this thesis is to implement a modular version of Partial Order Reduction such that other verifiers can also benefit from this technique.

Many verifiers are specialized for reachability properties. This work tries to express complex properties for concurrent programs as reachability.

Finding and fixing bugs is one of the most expensive parts of the software development process. To expedite it, a good description of all inputs which result in the same error can be helpful. To generate them, we will use CPAchecker to find constraints which result in an error when fulfilled, for example all even numbers as input result in an error. This will be done by first finding an error path in the program being analyzed, followed by refining a first guess for a constraint using an approach based on CEGAR.

Correctness Witnesses are an artifact produced by a verifier which allows a validator to replay the verification process. The task would be to analyze correctness witnesses and find semantically equivalent witnesses from the perspective of a validator.

CPAchecker is a very successfull tool for model checking. In particular it contains a lot of the components required to make use of it for taint analysis. The goal of this thesis would be to implement taint analysis in CPAchecker and evaluating it on a set of benchmarks.

Verifiers can proof different properties about many different programs. However, it is not clear how well they perform on real-world programs. The goal of this thesis would be to evaluate the performance of different verifiers on a set of real-world programs.

Verifiers can proof different properties about many different programs. However, it is not clear how well they perform on real-world programs. The goal of this thesis would be to evaluate the performance of different verifiers on a set of real-world programs.

Finding good predicates is a key challenge for verifying programs using predicate analysis. Currently some heuristics and interpolation techniques are used to find new predicates. On the other hand machine learning techniques have been succesfull in determining invariants for programs. The goal of this thesis would be to use the information generated during the exploration of the state-space of a program to find good predicates/interpolants using machine learning techniques.