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

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Silvio Ghilardi, Silvio Ranise
• Keywords: Artificial Intelligence, Backward Reachability Analysis, Invariant Synthesis, Infinite State Systems, TABLEAUX 2009