publication . Article . 2006

Termination Criteria for Bounded Model Checking: Extensions and Comparison

Awedh, Mohammad; Somenzi, Fabio;
Open Access English
  • Published: 01 Jan 2006 Journal: Electronic Notes in Theoretical Computer Science, issue 1, pages 51-66 (issn: 15710661, Copyright policy)
  • Publisher: Elsevier B.V.
Abstract
AbstractIncreasing 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 [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the li...
Subjects
free text keywords: Bounded model checking, Büchi automata, safety and liveness properties, termination conditions, Computer Science(all), Theoretical Computer Science, General Computer Science, Reachability, Cycle detection, Counterexample, Computer science, Discrete mathematics, Büchi automaton, Bounded function, Liveness, Model checking, Automaton
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue