Aachen University of Technology

Integration of Model Checking and Theorem Proving (IMCTP'01)

Affiliated Workshop of CONCUR'01

August 20th, 2001
Aalborg, Denmark

THE WORKSHOP HAS BEEN CANCELLED!

In the formal verification of software and hardware systems, two fundamental approaches to analyzing systems for desired properties are well established: model checking and theorem proving. The first relies on building a finite model of the system and automatically checking that it fulfills the property, essentially by an exhaustive state space search. In the theorem-proving approach, both the system and its desired properties are expressed as formulae in some logic. Here, the verification problem amounts to finding a proof of a property from the axioms. In contrast to model checking, theorem proving can directly deal with infinite state spaces by employing appropriate induction techniques.

Their formal strength makes them a powerful extension to traditional techniques like simulation and testing. This strength could most likely be extended even more by combining the automation used for checking finite state spaces and the generality of theorem provers, bringing model checking in the reach of unbounded state spaces and enabling more automation in the theorem proving approach. Specific examples of such a combination are

• the use of model checking as a decision procedure within a deductive framework,
• the extension of model checkers by proof assistants for decomposing a verification goal into model-checkable subgoals, and
• the application of theorem-proving methods to formally abstract infinite state spaces to finite-state form, followed by model checking.

Extended abstracts of up to five pages in PostScript or PDF should by submitted by email to imctp01@cs.rwth-aachen.de, not later than June 1st, 2001. Accepted abstracts are expected to be presented in a 30-minutes talk at the workshop. The proceedings will be published as a technical report of the Computer Science Department at Aachen University of Technology, and will be available at the workshop.

The authors of accepted abstracts will be invited to submit a full paper version, which will be reviewed according to scientific standards. A special issue of a journal containing the accepted papers is under negotiation.

IMCTP'01 will be integrated in the registration procedure of CONCUR'01.

Thomas Noll , 12.06.2001