Sciweavers

Share
CAV
2006
Springer

Yasm: A Software Model-Checker for Verification and Refutation

12 years 5 months ago
Yasm: A Software Model-Checker for Verification and Refutation
Example Guided Abstraction Refinement (CEGAR) [6] framework. A number of wellengineered software model-checkers are available, e.g., SLAM [1] and BLAST [12]. Why build another one? nal 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. A number of techniques for creating and combining over- and under-approximating ions have been proposed, e.g., [7, 9, 3, 15, 16]. In these approaches, model-checking yields either true or false, which are deemed to be conclusive,...
Arie Gurfinkel, Ou Wei, Marsha Chechik
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Arie Gurfinkel, Ou Wei, Marsha Chechik
Comments (0)
books