Termination Criteria for Bounded Model Checking: Extensions and Comparison

Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [1] we presented a criterion based on the translation of the linear-time specification into a B

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Mohammad Awedh, Fabio Somenzi
• Keywords: B¨uchi Automaton, ENTCS 2006, Fair Cycle, Termination Length