Advertisement
Published in:
2006 | OriginalPaper | Chapter
Yasm: A Software Model-Checker for Verification and Refutation
(Tool Paper)
Authors : Arie Gurfinkel, Ou Wei, Marsha Chechik
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper presents
Yasm
: a (yet another) software model-checker based on the Counter-Example Guided Abstraction Refinement (CEGAR) [6] framework. A number of well-engineered software model-checkers are available, e.g.,
Slam
[1] and
Blast
[12]. Why build another one?
Traditional software model-checkers build over-approximating abstractions of the programs they analyze and typically bias their analysis towards proving that a (safety) property of interest holds (verification). On the other hand, since model-checkers are widely known for their bug-finding abilities, they are often used for refutation. In this case, the above approach seems unreasonable: why introduce spurious behaviour and make it more difficult to find a real bug? For such circumstances, one would just want to prove that the property is false (refutation). No witness for that is required.