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.
The different versions of the original document can be found in:
Published on 01/01/2005
Volume 2005, 2005
DOI: 10.1109/date.2005.257
Licence: CC BY-NC-SA license
Are you one of the authors of this document?