Sciweavers

TABLEAUX
2009
Springer

Goal-Directed Invariant Synthesis for Model Checking Modulo Theories

13 years 9 months ago
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
We are interested in automatically proving safety properties of infinite state systems. We present a technique for invariant synthesis which can be incorporated in backward reachability analysis. The main theoretical result ensures that (under suitable hypotheses) our method is guaranteed to find an invariant if one exists. We also discuss heuristics that allow us to derive an implementation of the technique showing remarkable speed-ups on a significant set of safety problems in parametrised systems. c SpringerVerlag 2009
Silvio Ghilardi, Silvio Ranise
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TABLEAUX
Authors Silvio Ghilardi, Silvio Ranise
Comments (0)