System description using OBDD’s for the validation of skolem verification conditions

Abstract

The verification conditions associated with concurrent sys­tems and their invariants are usually instances of the VC-scheme, i.e., (formula presented) Besides, the following assumptions are often satisfied: 1. The set of hypotheses H = {h1, …, hn} is rather large; 2. The hypotheses and the conclusion are small quantifier-free formulas; 3. They are based on a large set of booleans and a smaller set of predi­cates; 4. If H |= c, then there is a small subset H0 ⊂ H such that H0 |= c. We demonstrate a specific, OBDD-based technique for validating in­stances of the VC-scheme. The main task of the tool is to construct an upper bound for H0, as tight as possible. The technique is illustrated with an example.