Software and Computational Systems Lab

Bounded Model Checking (BMC) is one of the most widely used techniques in software verification. One of the most popular BMC tools for C programs is CBMC. Currently it is a lot more efficient than CPAchecker's implementation of BMC. The goal of this thesis is to analyze why CPAchecker's BMC is slower than CBMC and to improve its performance.

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.

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.