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 all implementation of the technique showing remarkable speed-ups oil a significant set of safety problems in parametrised systems.
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories / Ghilardi, S; Ranise, S. - 5607:(2009), pp. 173-+. (Intervento presentato al convegno TABLEAUX '09: 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods tenutosi a Norway nel October 2009).
Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
Ranise, S
2009-01-01
Abstract
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 all implementation of the technique showing remarkable speed-ups oil a significant set of safety problems in parametrised systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
