Simulation-Directed Invariant Mining for Software Verification

13 years 4 months ago
Simulation-Directed Invariant Mining for Software Verification
With the advance of SAT solvers, transforming a software program to a propositional formula has generated much interest for bounded model checking of software in recent years. However, reasoning at the Boolean level often may not be able to identify some key relations among the original high-level program variables. In this paper, we propose a novel framework that uses simulation-directed data mining in the original program to extract a set of high-level potential property invariants according to the dynamic execution data of the software. When these learned invariants are added as constraints to the bounded model checking instances of the software, they help to significantly reduce the search space. The simulation-directed invariant mining framework exhibits more flexibility compared to the conventional static program analysis approaches, and the experimental results showed that our approach can lead to up to an order of magnitude of speedup in software verification via bounded model...
Xueqi Cheng, Michael S. Hsiao
Added 29 May 2010
Updated 29 May 2010
Type Conference
Year 2008
Where DATE
Authors Xueqi Cheng, Michael S. Hsiao
Comments (0)