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 Proceedings

Front Cover
Susanne Graf, Michael Schwartzbach
Springer Science & Business Media, Mar 15, 2000 - Computers - 552 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

On the Construction of Automata from Linear Arithmetic Constraints
1
An Extensible Type System for ComponentBased Design
20
A Generic Tool for Proof Development
38
Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation
43
Consistent Integration of Formal Methods
48
An Architecture for Interactive Program Provers
63
The PROSPER Toolkit
78
From Semantics to Tools
93
Checking for CFFDPreorder with Tester Processes
283
Fair Bisimulation
299
Integrating Low Level Symmetries into Reachability Analysis
315
Model Checking Support for the ASM HighLevel Language
331
A Markov Chain Model Checker
347
Model Checking SDL with Spin
363
Combining Constraint Solvers with BDDs for Automatic Invariant Checking
378
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation
395

On the Construction of Live Timed Systems
109
On MemoryBlock Traversal Problems in ModelChecking Timed Systems
127
Symbolic Model Checking for Rectangular Hybrid Systems
142
Efficient Data Structure for Fully Symbolic Verification of RealTime Software Systems
157
Verification of Parameterized Systems Using Logic Program Transformations
172
Abstracting WS1S Systems to Verify Parameterized Networks
188
A Tool for Expressing Validation Techniques over Infinite State Systems
204
Transitive Closures of Regular Relations for Verifying InfiniteState Systems
220
Using Static Analysis to Improve Automatic Test Generation
235
Efficient Diagnostic Generation for Boolean Equation Systems
251
Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems
266
Symbolic Reachability Analysis Based on SATSolvers
411
Symbolic Representation of UpwardClosed Sets
426
An Experimental Evaluation for Asynchronous Concurrent Systems
441
ToolBased Specification of Visual Languages and Graphic Editors
456
A Visual Editor and Compiler for vPromela
471
A Comparison of Two Verification Methods for Speculative Instruction Execution
487
Partial Order Reductions for Security Protocol Verification
503
Model Checking Security Protocols Using a Logic of Belief
519
A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors
535
Author Index
550
Copyright

Common terms and phrases

Bibliographic information