loading...
Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking
Munich, Germany March 07-March 11
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2005.93Design, Automation and Test in Europe ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Gianpiero Cabodi, Marco Crivellari, Sergio Nocco, Stefano Quer, "Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking," Design, Automation and Test in Europe Conference and Exhibition, vol. 2, pp. 688-689, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005.
 
 
BibTex
x
 
@article{ 10.1109/DATE.2005.93,
author = {Gianpiero Cabodi and Marco Crivellari and Sergio Nocco and Stefano Quer},
title = {Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking},
journal ={Design, Automation and Test in Europe Conference and Exhibition},
volume = {2},
year = {2005},
issn = {1530-1591},
pages = {688-689},
doi = {http://doi.ieeecomputersociety.org/10.1109/DATE.2005.93},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Design, Automation and Test in Europe Conference and Exhibition
TI - Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking
SN - 1530-1591
SP688
EP689
A1 - Gianpiero Cabodi,
A1 - Marco Crivellari,
A1 - Sergio Nocco,
A1 - Stefano Quer,
PY - 2005
KW - null
VL - 2
JA - Design, Automation and Test in Europe Conference and Exhibition
ER -
 
Gianpiero Cabodi, Politecnico di Torino, Italy
Marco Crivellari, Politecnico di Torino, Italy
Sergio Nocco, Politecnico di Torino, Italy
Stefano Quer, Politecnico di Torino, Italy
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.
Citation:
Gianpiero Cabodi, Marco Crivellari, Sergio Nocco, Stefano Quer, "Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking," date, vol. 2, pp.688-689, Design, Automation and Test in Europe (DATE'05) Volume 2, 2005
Usage of this product signifies your acceptance of the Terms of Use.