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) [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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Kamide, Norihiro: Falsification-aware semantics and sequent calculi for classical logic (2022)
  2. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  3. Beyene, Tewodros A.; Popeea, Corneliu; Rybalchenko, Andrey: Efficient CTL verification via Horn constraints solving (2016)
  4. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  5. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: Whale: an interpolation-based algorithm for inter-procedural verification (2012)
  6. Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
  7. Kaneiwa, Ken; Kamide, Norihiro: Paraconsistent computation tree logic (2011)
  8. Wei, Ou; Gurfinkel, Arie; Chechik, Marsha: On the consistency, expressiveness, and precision of partial modeling formalisms (2011)
  9. Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
  10. Meller, Yael; Grumberg, Orna; Shoham, Sharon: A framework for compositional verification of multi-valued systems via abstraction-refinement (2009)
  11. Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant: Verification of evolving software via component substitutability analysis (2008)
  12. Gurfinkel, Arie; Wei, Ou; Chechik, Marsha: Model checking recursive programs with exact predicate abstraction (2008)
  13. Gurfinkel, Arie; Chechik, Marsha: Why waste a perfectly good abstraction? (2006)
  14. Gurfinkel, Arie; Wei, Ou; Chechik, Marsha: Yasm: a software model-checker for verification and refutation (2006) ioport