HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Multi-Object Checking Counterexamples

Abstract : Model checking has become the most widely used technique for the verification of state based systems. In addition to its automation in checking whether a system model satisfies a specification, model checking provides a counterexample trace if the checking condition does not hold. Such a sequence of states illustrates how the model falsifies the specification. Multi-object checking utilizes model checking as the underlying verification technique for each object so that the verification of a system is only limited by the state space of the largest object. Our contribution proposes an enhancement to multi-object checking -- the automated generation of a global system trace, if a specification in multi-object logic does not hold.
Document type :
Conference papers
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, September 6, 2006 - 7:19:10 PM
Last modification on : Friday, November 19, 2021 - 12:42:03 PM
Long-term archiving on: : Monday, April 5, 2010 - 11:02:29 PM


  • HAL Id : inria-00091663, version 1



Maik Kollmann, Yuen Man Hon. Multi-Object Checking Counterexamples. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.163-167. ⟨inria-00091663⟩



Record views


Files downloads