Towards SMT Model-Checking of Array-based Systems

Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.

doi:10.1007/978-3-540-71070-7_6

IRIS Institutional Research Information System - AIR Archivio Istituzionale della Ricerca

IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Milano.

AIR nasce in UNIMI nel 2006 con lo scopo di raccogliere, documentare e conservare le informazioni sulla produzione scientifica dell'Università degli Studi di Milano e costituisce di fatto l'Anagrafe della ricerca dell'Ateneo.

We introduce the notion of array-based system as a suitable abstraction of infinite state systems such as broadcast protocols or sorting programs. By using a class of quantified-first order formulae to symbolically represent array-based systems, we propose methods to check safety (invariance) and liveness (recurrence) properties on top of Satisfiability Modulo Theories solvers. We find hypotheses under which the verification procedures for such properties can be fully mechanized.

Titolo:	Towards SMT Model-Checking of Array-based Systems
Autori:	GHILARDI, SILVIO (Primo) NICOLINI, ENRICA (Secondo) S. Ranise ZUCCHELLI, DANIELE (Ultimo) mostra contributor esterni nascondi contributor esterni
Parole Chiave:	model checking ; satisfiability modulo theory
Settore Scientifico Disciplinare:	Settore M-FIL/02 - Logica e Filosofia della Scienza
Data di pubblicazione:	2008
Digital Object Identifier (DOI):	10.1007/978-3-540-71070-7_6
Tipologia:	Book Part (author)
Appare nelle tipologie:	03 - Contributo in volume

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/2434/53456

Citazioni

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.