Abstract
The interplay back and forth between software model checking and hardware model checking has been fruitful for both. Originally intended for the analysis of concurrent software, model checking was first used in hardware verification. The abstraction methods developed for hardware verification however have been a stepping stone for the new generation of software verification tools including SLAM, BLAST, and MAGIC which focus on control-intensive software in C. Most recently, the experience with software verification is providing new leverage for verifying hardware designs in high level languages. © IFIP International Federation for Information Processing 2008.
Cite
CITATION STYLE
Clarke, E., Gupta, A., Jain, H., & Veith, H. (2008). Model checking: Back and forth between hardware and software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4171 LNCS, pp. 251–255). https://doi.org/10.1007/978-3-540-69149-5_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
