CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishWe 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Goal-Directed Invariant Synthesis for Model Checking Modulo Theories | |
| Autori: | ||
| Data di pubblicazione: | 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. | |
| Handle: | http://hdl.handle.net/11582/22074 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11582/22074
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Copyright © 2021