“Efficient SAT-Based Bounded Model Checking of Evolving Systems” by Sophie Andrews, Matthew Sotoudeh, and Clark Barrett. In Proceedings of Design, Automation & Test in Europe Conference (DATE '25), Apr. 2025. Lyon, France.
SAT-based verification is a common technique used by industry practitioners to find bugs in computer systems. However, these systems are rarely designed in a single step: instead, designers repeatedly make small modifications, reverifying after each change. With current tools, this reverification step takes as long as a full, from-scratch verification, even if the design has only been modified slightly. We propose a novel SAT-based verification technique that performs significantly better than the naÃ&hibar;ve approach in the setting of evolving systems. The key idea is to reuse information learned during the verification of earlier versions of the system to speed up the verification of later versions. We instantiate our technique in a bounded model checking tool for SystemVerilog code and apply it to a new benchmark set based on real edit history for a set of open source RISC-V cores. This new benchmark set is now publicly available for further research on verification of evolving systems. Our tool, PrediCore, significantly improves the time required to verify properties on later versions of the cores compared to the current state-of-the-art, verify-from-scratch approach.
BibTeX entry:
@inproceedings{ASB25,
author = {Sophie Andrews and Matthew Sotoudeh and Clark Barrett},
title = {Efficient SAT-Based Bounded Model Checking of Evolving Systems},
booktitle = {Proceedings of Design, Automation {&} Test in Europe
Conference (DATE '25)},
publisher = {IEEE},
month = apr,
year = {2025},
doi = {10.23919/DATE64628.2025.10993135},
note = {Lyon, France},
url = {http://theory.stanford.edu/~barrett/pubs/ASB25.pdf}
}
(This webpage was created with bibtex2web.)