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.

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Mohammad Awedh, Fabio Somenzi
• Keywords: CAV 2004, Formal Methods, LTL Formula, Model Checking, Termination Criterion