Proving More Properties with Bounded Model Checking

12 years 5 months ago
Proving More Properties with Bounded Model Checking
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 B¨uchi 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.
Mohammad Awedh, Fabio Somenzi
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Mohammad Awedh, Fabio Somenzi
Comments (0)