Tools and Algorithms for the Construction and Analysis of Systems

1. Front Matter

   Pages I-XIV

   PDF

2. Invited Contribution

   1. On the Construction of Automata from Linear Arithmetic Constraints

      • Pierre Wolper, Bernard Boigelot

      Pages 1-19

3. Software and Formal Methods Tools

   1. An Extensible Type System for Component-Based Design

      • Yuhong Xiong, Edward A. Lee

      Pages 20-37

   2. Proof General: A Generic Tool for Proof Development

      • David Aspinall

      Pages 38-43

   3. ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation

      • Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer

      Pages 43-47

4. Formal Methods Tools

   1. Consistent Integration of Formal Methods

      • Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch

      Pages 48-62

   2. An Architecture for Interactive Program Provers

      • Jörg Meyer, Arnd Poetzsch-Heffter

      Pages 63-77

   3. The PROSPER Toolkit

      • Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson et al.

      Pages 78-92

   4. CASL: From Semantics to Tools

      • Till Mossakowski

      Pages 93-108

5. Timed and Hybrid Systems

   1. On the Construction of Live Timed Systems

      • Sébastien Bornot, Gregor Gößler, Joseph Sifakis

      Pages 109-126

   2. On Memory-Block Traversal Problems in Model-Checking Timed Systems

      • Fredrik Larsson, Paul Pettersson, Wang Yi

      Pages 127-141

   3. Symbolic Model Checking for Rectangular Hybrid Systems

      • Thomas A. Henzinger, Rupak Majumdar

      Pages 142-156

   4. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

      • Farn Wang

      Pages 157-171

6. Infinite and Parameterized Systems

   1. Verification of Parameterized Systems Using Logic Program Transformations

      • Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka

      Pages 172-187

   2. Abstracting WS1S Systems to Verify Parameterized Networks

      • Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl

      Pages 188-203

   3. FMona: A Tool for Expressing Validation Techniques over Infinite State Systems

      • J.-P. Bodeveix, M. Filali

      Pages 204-219

   4. Transitive Closures of Regular Relations for Verifying Infinite-State Systems

      • Bengt Jonsson, Marcus Nilsson

      Pages 220-235

7. Diagnostic and Test Generation

   1. Using Static Analysis to Improve Automatic Test Generation

      • Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu

      Pages 235-250

   2. Efficient Diagnostic Generation for Boolean Equation Systems

      • Radu Mateescu

      Pages 251-265

8. Efficient Model-Checking

   1. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems

      • Jean-Pierre Krimm, Laurent Mounier

      Pages 266-282

This book constitutes the refereed proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, held as part of ETAPS 2000 in Berlin, Germany, in March/April 2000.
The 33 revised full papers presented together with one invited paper and two short tool descriptions were carefully reviewed and selected from a total of 107 submissions. The papers are organized in topical sections on software and formal methods, formal methods, timed and hybrid systems, infinite and parameterized systems, diagnostic and test generation, efficient model checking, model-checking tools, symbolic model checking, visual tools, and verification of critical systems.

• SPIN
• Systems design
• algorithm
• algorithms
• automata
• data structure
• development tools
• formal method
• formal methods
• hybrid systems
• logic
• model checking
• systems analysis
• systems verification
• verification tools
• algorithm analysis and problem complexity

• VERIMAG, Gières, France

  Susanne Graf

• BRICS, Department of Computer Science, University of Aarhus, Aarhus C, Denmark

  Michael Schwartzbach

Policies and ethics