Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a "light-weight" algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach. © 2009 Elsevier B.V. All rights reserved.
Light-Weight SMT-based Model Checking / Ghilardi, S.; Ranise, S.; Valsecchi, T.. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 250:2(2009), pp. 85-102. (Intervento presentato al convegno Eighth International Workshop on Automated Verification of Critical Systems (AVoCS 08) tenutosi a Regno Unito nel 30/09-01/10-2008) [10.1016/j.entcs.2009.08.019].
Light-Weight SMT-based Model Checking
Ranise S.;
2009-01-01
Abstract
Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a "light-weight" algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach. © 2009 Elsevier B.V. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
