## 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 ProceedingsSusanne Graf, Michael Schwartzbach 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 |

550 | |

### Common terms and phrases

abstract action algorithm analysis application automata automaton behavior belief atoms bisimilar bisimulation boolean buffer CASL checker clock components Computer Aided Verification Computer Science concurrent constraints construction counterexample deallocation defined definition denote diagrams E.M. Clarke editor encoding equivalence example execution finite finite-state formal formula function given global graph IEEE implementation input integer interface invariant Isabelle/HOL iteration K1 and K2 language livelock LNCS method model checking module MTBDDs nodes operations parameterized partial order reduction Petri Nets Presburger arithmetic problem Proc Promela properties propositional protocol proving reachability relation represent representation Salsa satisfies Section semantics sequence sharing tree specification Spin Springer-Verlag structure symbolic model checking symmetry synchronization techniques temporal logic theorem prover tion tool transformation transition relation transition system transitive closure variables verification WS1S µ-calculus