Sciweavers

Share
VSTTE
2005
Springer

Model Checking: Back and Forth between Hardware and Software

9 years 3 months ago
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...
Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, He
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where VSTTE
Authors Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith
Comments (0)
books