Tools and Algorithms for the Construction and Analysis of Systems : 6th International Conference, TACAS 2000 Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 - April 2, 2000 Proceeding

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. On the Construction of Automata from Linear Arithmetic Constraints....Pages 1-19 An Extensible Type System for Component-Based Design....Pages 20-37 Proof General: A Generic Tool for Proof Development....Pages 38-43 ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation....Pages 43-47 Consistent Integration of Formal Methods....Pages 48-62 An Architecture for Interactive Program Provers....Pages 63-77 The PROSPER Toolkit....Pages 78-92 CASL: From Semantics to Tools....Pages 93-108 On the Construction of Live Timed Systems....Pages 109-126 On Memory-Block Traversal Problems in Model-Checking Timed Systems....Pages 127-141 Symbolic Model Checking for Rectangular Hybrid Systems....Pages 142-156 Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems....Pages 157-171 Verification of Parameterized Systems Using Logic Program Transformations....Pages 172-187 Abstracting WS1S Systems to Verify Parameterized Networks....Pages 188-203 FMona: A Tool for Expressing Validation Techniques over Infinite State Systems....Pages 204-219 Transitive Closures of Regular Relations for Verifying Infinite-State Systems....Pages 220-235 Using Static Analysis to Improve Automatic Test Generation....Pages 235-250 Efficient Diagnostic Generation for Boolean Equation Systems....Pages 251-265 Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems....Pages 266-282 Checking for CFFD-Preorder with Tester Processes....Pages 283-298 Fair Bisimulation....Pages 299-314 Integrating Low Level Symmetries into Reachability Analysis....Pages 315-330 Model Checking Support for the ASM High-Level Language....Pages 331-346 A Markov Chain Model Checker....Pages 347-362 Model Checking SDL with Spin....Pages 363-377 Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking....Pages 378-395 Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation....Pages 395-410 Symbolic Reachability Analysis Based on SAT-Solvers....Pages 411-425 Symbolic Representation of Upward-Closed Sets....Pages 426-441 BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems....Pages 441-456 Tool-Based Specification of Visual Languages and Graphic Editors....Pages 456-470 VIP: A Visual Editor and Compiler for v-Promela ....Pages 471-486 A Comparison of Two Verification Methods for Speculative Instruction Execution....Pages 487-502 Partial Order Reductions for Security Protocol Verification....Pages 503-518 Model Checking Security Protocols Using a Logic of Belief....Pages 519-534 A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors....Pages 535-549

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.