Yasm: A Software Model-Checker for Verification and Refutation. This paper presents Yasm: a (yet another) software model-checker based on the Counter-Example Guided Abstraction Refinement (CEGAR)  framework. A number of well-engineered software model-checkers are available, e.g., Slam  and Blast . 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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
- Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
- Kaneiwa, Ken; Kamide, Norihiro: Paraconsistent computation tree logic (2011)
- Wei, Ou; Gurfinkel, Arie; Chechik, Marsha: On the consistency, expressiveness, and precision of partial modeling formalisms (2011)
- Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
- Meller, Yael; Grumberg, Orna; Shoham, Sharon: A framework for compositional verification of multi-valued systems via abstraction-refinement (2009)
- Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant: Verification of evolving software via component substitutability analysis (2008)
- Gurfinkel, Arie; Chechik, Marsha: Why waste a perfectly good abstraction? (2006)