Trace Abstraction with Maximal Causality Reduction

Abstract

We are interested in the verification of concurrent programs with trace abstraction. Trace abstraction takes a trace (i.e. a sequence of actions) leading to the error location and checks it for feasibility. If the trace is infeasible, we generalize it to an automaton and subtract these traces from the program graph. This way we continue until we cannot get any more error traces. If that is the case, we have proven that the program cannot reach its error location.

Concurrent programs consist of different threads where at any point of time a statement of an arbitrary thread is executed. For the verification of concurrent programs we need to consider all these interleaving executions. This might lead to a problem, as there are usually many possible executions of the different threads. However some of them might be equivalent, i.e. their execution leads to the same program state. Trace abstraction usually needs to analyse various equivalent traces and therefore needs several redundant iterations. For that reason we try to reduce the number of analysed traces using maximal causal reduction to improve trace abstraction on concurrent programs.

Maximal causality reduction (MCR) is a technique to reduce the number of visited traces. We start with one trace and generate new non-equivalent permutations of that trace, i.e. traces with the same actions in a different order. Here two traces are equivalent if all read accesses of variables read the same value. MCR encodes the constraints of a trace in a formula which is called maximum causal model. This formula is then checked for satisfiability by a SMT-solver. A solution of this formula corresponds to a new trace.

TODO

• completed tasks, solved problems
• open problems, next steps
• literature references