Dagstuhl Seminar 03171
Deduction and Infinite-state Model Checking
( Apr 21 – Apr 25, 2003 )
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/03171
Organizers
- Deepak Kapur (University of New Mexico - Albuquerque, US)
- Andreas Podelski (MPI für Informatik - Saarbrücken, DE)
- Andrei Voronkov (University of Manchester, GB)
Contact
Q: In `infinite model checking', what is infinite, the model or the checking?
A: Both.
Model checking is an automated method to verify runtime properties of programs. Finite model checking applies to finite abstractions of software systems. Often, the task of constructing appropriate finite abstractions manually is hard, if not impossible. Therefore, a recent and promising research direction aims at infinite model checking. Here, deduction takes the central role in accounting for the infiniteness that arises from the direct modelling of software systems.
So far, the deduction problems arising in this context have been addressed in an adhoc manner by the model checking community. It is interesting to explore where existing techniques can be applied and where new kinds of research questions are raised.
For finite systems, model checking is based on Boolean logic. For many of the classes of systems with specific characteristics for infinite data and infinite control, the question for the right logic is still open (right in terms appropriate expressiveness and computational cost). It will be useful to classify the deduction problems corresponding to the different classes of systems.
Data: What classes of formulas are best used to account for classes of operations over classical domains such as integers? What are the new domains to model pointer structures, lists, queues, abstract data types in general?
Control: Advanced control (recursion, concurrency, threads, dynamic objects with changing communication patterns, mobility of computational agents, ) requires models of process terms with specific algebraic laws (for stack concatenation, parallel composition, ); which ones exactly?
For safety properties, model checking amounts to automatically synthesising inductive invariants, by fixpoint iteration. For infinite model checking, the application of the fixpoint operator, the fixpoint test and the extrapolation of intermediate results each are theorem proving tasks. What are the demands, the functionality, and the evaluation criteria for theorem provers that are called during fixpoint iteration?
For example, the performance of a possibly incomplete decision tool for the validity of implication (used for the fixpoint termination test) determines a tradeoff where the fixpoint iteration terminates after either few but possibly expensive steps or cheap but possibly numerous steps.
Extrapolation of intermediate results during fixpoint iteration is required for accelerating or enforcing termination. The abstract interpretation framework of Cousot and Cousot formulates abstraction techniques at a semantic level. Their instantiation to syntax-based theorem provers is still not obvious.
There are many more possible topics to be discussed at our workshop...
- Alessandro Armando (University of Genova, IT) [dblp]
- Franz Baader (TU Dresden, DE) [dblp]
- Peter Baumgartner (MPI für Informatik - Saarbrücken, DE) [dblp]
- Christoph Benzmüller (Universität des Saarlandes, DE) [dblp]
- Wolfgang Bibel (TU Darmstadt, DE)
- Bernard Boigelot (University of Liège, BE) [dblp]
- Maria Paola Bonacina (University of Verona, IT) [dblp]
- Ahmed Bouajjani (University Paris-Diderot, FR) [dblp]
- Tevfik Bultan (University of California - Santa Barbara, US)
- Hans de Nivelle (MPI für Informatik - Saarbrücken, DE) [dblp]
- Anatoli Degtyarev (King's College London, GB)
- Amy Felty (University of Ottawa, CA) [dblp]
- Ulrich Furbach (Universität Koblenz-Landau, DE) [dblp]
- Harald Ganzinger (MPI-SWS - Saarbrücken, DE)
- Martin Giese (Chalmers UT - Göteborg, SE) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Thomas Hillenbrand (MPI für Informatik - Saarbrücken, DE)
- Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
- Yevgeny Kazakov (MPI für Informatik - Saarbrücken, DE) [dblp]
- Konstantin Korovin (University of Manchester, GB) [dblp]
- Axel Legay (University of Liège, BE) [dblp]
- Alexander Leitsch (TU Wien, AT) [dblp]
- Reinhold Letz (TU München, DE)
- David McAllester (TTIC - Chicago, US)
- William McCune (Argonne National Laboratory, US)
- Aart Middeldorp (University of Tsukuba, JP) [dblp]
- Marius Minea (Polytechnical University - Timisoara, RO)
- Robert Nieuwenhuis (UPC - Barcelona, ES) [dblp]
- David A. Plaisted (University of North Carolina at Chapel Hill, US)
- Andreas Podelski (MPI für Informatik - Saarbrücken, DE) [dblp]
- Silvio Ranise (INRIA Lorraine - Nancy, FR)
- Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
- Julian Richardson (NASA / RIACS - Moffett Field, US)
- Albert Rubio (UPC - Barcelona, ES) [dblp]
- Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
- Renate Schmidt (University of Manchester, GB) [dblp]
- Manfred Schmidt-Schauss (Universität Frankfurt, DE) [dblp]
- Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
- Stephan Schulz (TU München, DE) [dblp]
- Sanjit A. Seshia (Carnegie Mellon University - Pittsburgh, US) [dblp]
- John Slaney (Australian National University - Canberra, AU)
- Gernot Stenz (TU München, DE)
- Mark Stickel (SRI - Menlo Park, US)
- Mahadevan Subramaniam (University of Nebraska, US)
- Wolfgang Thomas (RWTH Aachen, DE) [dblp]
- Ashish Tiwari (SRI - Menlo Park, US) [dblp]
- Helmut Veith (TU München, DE) [dblp]
- Robert Veroff (University of New Mexico - Albuquerque, US)
- Andrei Voronkov (University of Manchester, GB) [dblp]
Related Seminars
- Dagstuhl Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
- Dagstuhl Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
- Dagstuhl Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
- Dagstuhl Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
- Dagstuhl Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
- Dagstuhl Seminar 05431: Deduction and Applications (2005-10-23 - 2005-10-28) (Details)
- Dagstuhl Seminar 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (Details)
- Dagstuhl Seminar 09411: Interaction versus Automation: The two Faces of Deduction (2009-10-04 - 2009-10-09) (Details)
- Dagstuhl Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
- Dagstuhl Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
- Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
- Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (Details)
- Dagstuhl Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
- Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
