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,...

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Arie Gurfinkel, Ou Wei, Marsha Chechik
• Keywords: CAV 2006, Example Guided Abstraction, Hardware, Software Model-checkers, Wellengineered Software Model-checkers