Software and Computational Systems Lab

Dual Approximated Reachability (DAR) is an interpolation-based verification algorithm that combines forward and backward reachability analysis. The goal is to have this algorithm implemented in CPAchecker and evaluate it against other verification approaches over the SV-COMP benchmark set.

In most verification tools, the reachability analysis searches for a path from the initial program location to the error location. The analysis could also be done backward, i.e. tries to reach the initial location from the error location. The goal of this project is to implement a control-flow automata (CFA) transformer in CPAchecker that reverses program executions by following the transitions backward. One could then apply existing analysis to verify the reverse CFA.

Background: Btor2 is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers or testers.
Goal: The goal of the project is to compare the performance between software and hardware analyzers and try to improve Btor2C based on the findings. A few possible directions are

• Analyze the performance difference between software and hardware verifiers
• Define a customized C annotation for bit-precise integer/bit-vector encoding, and have it implemented in Btor2C and CPAchecker
• Improve Btor2C array encoding (see https://gitlab.com/sosy-lab/software/btor2c/-/issues/17)
• Support witness format conversion in Btor2C

Symbolic execution is a well-known software analysis technique that searches for execution paths that could lead to the error location from the initial program location. Backward symbolic execution, on the contrary, follows the execution backward and searches paths from the error location to the initial location. The goal of the project is to implement such technique in CPAchecker.

Single-loop transformation is a process that converts a program with an arbitrary loop structure (, which may contain nested and/or multiple loops) to an equivalent program with only one loop. Though such transformation already exists in CPAchecker, we would like to re-implement it with the new control-flow automata transformer, which provides more useful features and functionalities.

The idea is to mutate (e.g. by negating the assertions) the tasks in SV-COMP benchmark set, and see if the verifiers still deliver the expected results on the mutated tasks. If not, it indicates that the tool might be unsound, or the verdicts might be incorrect. In either case, we could improve the robustness of SV-COMP.