Abstract

Submitted on behalf of EDAA (http://www.edaa.com/); International audience; While most of the effort in improving verification times for pipeline machine verification has focused on faster decision procedures, we show that the refinement maps used also have a drastic impact on verification times. We introduce a new class of refinement maps for pipelined machine verification, and using the state-of-the-art verification tools UCLID and Siege we show that one can attain several orders of magnitude improvements in verification times over the standard flushing-based refinement maps, even enabling the verification of machines that are too complex to otherwise automatically verify.


Original document

The different versions of the original document can be found in:

https://dl.acm.org/citation.cfm?id=1049315,
https://ieeexplore.ieee.org/document/1395773,
http://ieeexplore.ieee.org/document/1395773,
http://dx.doi.org/10.1109/DATE.2005.257,
http://www.cecs.uci.edu/~papers/date05/papers/2005/date05/pdffiles/10e_2.pdf,
https://hal.archives-ouvertes.fr/hal-00181307,
https://hal.archives-ouvertes.fr/hal-00181307/document,
https://academic.microsoft.com/#/detail/2109939657
http://dx.doi.org/10.1109/date.2005.257
https://hal.archives-ouvertes.fr/hal-00181307/document,
https://hal.archives-ouvertes.fr/hal-00181307/file/228821304.pdf
Back to Top

Document information

Published on 01/01/2005

Volume 2005, 2005
DOI: 10.1109/date.2005.257
Licence: CC BY-NC-SA license

Document Score

0

Views 0
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?