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
Abstract
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
https://link.springer.com/cont...
Part of book or chapter of book
Provider: UnpayWall
http://www.springerlink.com/in...
Part of book or chapter of book . 2010
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue