publication . Part of book or chapter of book . 2010

Proving More Properties with Bounded Model Checking

Mohammad Awedh; Fabio Somenzi;
Open Access
  • Published: 14 Sep 2010
  • Publisher: Springer Berlin Heidelberg
Bounded Model Checking, although complete in theory, has been thus far limited in practice to falsification of properties that were not invariants. In this paper we propose a termination criterion for all of LTL, and we show its effectiveness through experiments. Our approach is based on converting the LTL formula to a Buchi automaton so as to reduce model checking to the verification of a fairness constraint. This reduction leads to one termination criterion that applies to all formulae. We also discuss cases for which a dedicated termination test improves bounded model checking efficiency.
Download from
Part of book or chapter of book
Provider: UnpayWall
Part of book or chapter of book . 2010
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue