Archivio Istituzionale della RicercaIn 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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/1848894
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo