A Combination of Forward and Backward Reachability Analysis Methods

摘要

Induction-guided falsification (IGF) is a combination of bounded model checking (BMC) and structural induction, which can be used for falsification of invariants. IGF can also be regarded as a combination of forward and backward reachability analysis methods. This is because BMC is a forward reachability analysis method and structural induction can be regarded as a backward reachability analysis method. We report on a case study in which a variant of IGF has been used to systematically find a counterexample showing that NSPK does not enjoy the agreement property.