Model Checking: Back and Forth between Hardware and Software

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 veron. 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 embedded systems. Most recently, the experience with software verification is currently providing new leverage for verifying hardware designs in high level languages. 1 From Software Verification to Hardware Verification The origins of model checking date back to the early 1980s, when Clarke and Emerson [5] and, independently, Queille and Sifakis [19] introduced a new algorithmic approach for the verification of computer systems. Their approach amounts to checking the satisfaction of a logical specification over a system model which...

• Type: Conference
• Year: 2005
• Where: VSTTE
• Authors: Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith
• Keywords: Hardware Model Checking, Model Checking, Software Engineering, Software Model Checking, VSTTE 2005