Software and Computational Systems Lab

Verifying complex programs with respect to a given specification (e.g., 'check that function reach_error is never called') may be time consuming. To make verifiers more applicable in industry, we want to tackle the problem with a divide-and-conquer approach. We decompose the verification task in multiple smaller tasks that are then verified in parallel. As soon as one of the analyses reports a violation, we abort all other analyses and report the violation. This will lead to many false alarms since we do not know with which input parameters functions will be called. Return values of functions will be ignored and interpreted as unknown value in a first step. From there we can continue in two directions:

1. Analyze functions under a user defined condition (e.g., a user restricts the values of parameter x of function foo to the interval [0;100])
2. We identify each function call automatically and try to infer all parameters.

1. The verification verdict should be available faster (in terms of passed walltime).
2. Wrong proofs should be non-existing. In case a program is safe, the decomposition should be a sound over-approximation.

Verifiers are able to tell whether a given task is safe or faulty with respect to a given specification. However, it does not provide enough information to immediately fix the bug. To mitigate this drawback, we want to apply automatic program repair to unsafe tasks. Given a program that violates a given specification we want to synthesize a patch for the program such that the same faulty behavior cannot be observed anymore.

There might be several reasons for reaching a specific error location in a program. We want to identify all classes of inputs that trigger the same bug. They should be as abstract as possible but as precise as necessary. For a given program we want to find out, which restrictions to nondeterministic variables are necessary to reach an error location. For example, we might reach error location E1, if the nondeterministic variable x equals 1 and the nondeterministic variable y is less than 1024. Error location E2 might be reachable for x > 100 and y < 100. Otherwise the program does not show faulty behavior. In our approach we are interested in the most abstract restrictions for all inputs for reaching error locations instead of a single testvector like x = 1 & y = 1023 for E1 and/or x = 101 & y = 99 for E2.

CPAchecker is a framework for automatic software verification developed at our chair. As such it has a broad technology stack that should provides everything that is needed for verifying C programs. CPAchecker is able to distribute the analysis of a single task to different workers by decomposing the input program into blocks. Each worker analyzes one block and communicates the results to all other workers over messages to establish the correct verification result. In case we find a violation, fault localization can help to explain the root cause of the error. There already exist several techniques of fault localization in CPAchecker. Unfortunately, some of them may take long since they have to check 2^n possibilities in the worst-case scenario. By distributing fault localization to the relevant workers, 'n' shrinks since they work on smaller blocks. We expect a performance boost for fault localization after distributing it.

CPAchecker is a framework for automatic software verification developed at our chair. As such it has a broad technology stack that should provides everything that is needed for verifying C programs. CPAchecker is able to distribute the analysis of a single task to different workers by decomposing the input program into blocks. Each worker analyzes one block and communicates the results to all other workers over messages to establish the correct verification result. In case we find a violation, we want to provide the user with a counterexample that proves the reachability of a violation. Currently, neither the counterexample nor invariants can be synthesized from the messages. However, witnesses are important for improving the trust in the verfication results.