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.
Goal-directed invariant synthesis for model checking modulo theories / S. Ghilardi, S. Ranise - In: Automated reasoning with analytic tableaux and related methods : 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009 : Proceedings / [a cura di] M. Giese, A. Waaler. - Berlin : Springer, 2009. - ISBN 9783642027154. - pp. 173-188 (( Intervento presentato al 18th. convegno TABLEAUX tenutosi a Oslo nel 2009 [10.1007/978-3-642-02716-1_14].
Goal-directed invariant synthesis for model checking modulo theories
S. GhilardiPrimo
;
2009
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 an implementation of the technique showing remarkable speed-ups on a significant set of safety problems in parametrised systems.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
