Abstract:
We present a technique for verifying concurrent software systems via SAT-based three-valued bounded model checking. It is based on a direct transfer of the system to be analysed and a temporal logic property into a propositional logic formula that encodes the corresponding model checking problem. In our approach we first employ three-valued abstraction which gives us an abstract system defined over predicates with the possible truth values true, false and unknown. The state space of the abstract system is then logically encoded. The verification result of the encoded three-valued model checking problem can be obtained via two satisfiability checks, one for an over-approximation of the encoding and one for an under-approximation. True and false results can be immediately transferred to the system under consideration.
In case of an unknown result, the current abstraction is too imprecise for a definite outcome. In order to achieve the necessary precision, we have developed a novel cause-guided abstraction refinement procedure. An unknown result always entails a truth assignment that only satisfies the over-approximation, but not the under-approximation. We determine the propositional logic clauses of the under-approximation that are not satisfied under the assignment. These clauses contain unknown as a constant. Each unknown is associated with a cause of uncertainty that refers to missing predicates that are required for a definite model checking result. Our procedure adds these predicates to the abstraction and constructs the encoding corresponding to the refined model checking problem. The procedure is iteratively applied until a definite result can be obtained.
We have integrated our novel refinement approach into a SAT-based three-valued bounded model checker. In an experimental evaluation, we show that our approach allows to automatically and quickly reach the right level of abstraction for solving software verification tasks.
