publication . Part of book or chapter of book . 2004

Proving more properties with bounded model checking

Mohammad Awedh; Somenzi, F.; Alur, R.; Peled, Da;
  • Published: 01 Jan 2004
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.
Subjects
arXiv: Computer Science::Formal Languages and Automata TheoryComputer Science::Logic in Computer Science
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: Büchi automaton, Propositional formula, Bounded function, Linear logic, Algorithm, Computer science, Model checking, Abstraction model checking, Temporal logic, Automaton
Related Organizations
Download fromView all 2 versions
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
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue