In this paper a non-canonical circuit-based state set representation is used to efficiently perform quantifier elimination. The novelty of this approach lies in adapting equivalence checking and logic synthesis techniques, to the goal of compacting circuit based state set representations resulting from existential quantification. The method can be efficiently combined with other verification approaches such as inductive and SAT-based pre-image verifications.

Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking / Cabodi, Gianpiero; M., Crivellari; Nocco, Sergio; Quer, Stefano. - STAMPA. - (2005), pp. 688-689. (Intervento presentato al convegno ACM/IEEE Design, Automation and Test in Europe Conference and Exhibition (DATE 2005) tenutosi a Munich, Germany nel 7-11 March 2005).

Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking

CABODI, Gianpiero;NOCCO, SERGIO;QUER, Stefano
2005

Abstract

In this paper a non-canonical circuit-based state set representation is used to efficiently perform quantifier elimination. The novelty of this approach lies in adapting equivalence checking and logic synthesis techniques, to the goal of compacting circuit based state set representations resulting from existential quantification. The method can be efficiently combined with other verification approaches such as inductive and SAT-based pre-image verifications.
2005
0769522882
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1848894
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo