Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2–6, 2001 Proceedings

Moshe Y. Vardi (auth.), Tiziana Margaria, Wang Yi (eds.)3540418652, 9783540418658

This book constitutes the refereed proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001.
The 36 revised full papers presented together with an invited contribution were carefully reviewed and selected from a total of 125 submissions. The papers are organized in sections on symbolic verification, infinite state systems – deduction and abstraction, application of model checking techniques, timed and probabilistic systems, hardware – design and verification, software verification, testing – techniques and tools, implementation techniques, semantics and compositional verification, logics and model checking, and ETAPS tool demonstration.

---

Table of contents :
Branching vs. Linear Time: Final Showdown….Pages 1-22
Propositional Reasoning….Pages 23-23
Language Containment Checking with Nondeterministic BDDs….Pages 24-38
Satisfiability Checking Using Boolean Expression Diagrams….Pages 39-51
A Library for Composite Symbolic Representations….Pages 52-66
Synthesis of Linear Ranking Functions….Pages 67-81
Automatic Deductive Verification with Invisible Invariants….Pages 82-97
Incremental Verification by Abstraction….Pages 98-112
A Technique for Invariant Generation….Pages 113-127
Model Checking Syllabi and Student Careers….Pages 128-142
Verification of Vortex Workflows….Pages 143-157
Parameterized Verification of Multithreaded Software Libraries….Pages 158-173
Efficient Guiding Towards Cost-Optimality in UPPAAL….Pages 174-188
Linear Parametric Model Checking of Timed Automata….Pages 189-203
Abstraction in Probabilistic Process Algebra….Pages 204-219
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders….Pages 220-235
Hardware/Software Co-design Using Functional Languages….Pages 236-251
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors….Pages 252-267
Boolean and Cartesian Abstraction for Model Checking C Programs….Pages 268-283
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs….Pages 284-298
The loop Compiler for Java and JML….Pages 299-312
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking….Pages 313-327
Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation….Pages 328-342
Automated Test Generation from Timed Automata….Pages 343-357
Testing an Intentional Naming Scheme Using Genetic Algorithms….Pages 358-372
Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions….Pages 373-388
TATOO: T esting and A nalysis T ool for O bject- O riented Software….Pages 389-403
Implementing a Multi-valued Symbolic Model Checker….Pages 404-419
Is There a Best Symbolic Cycle-Detection Algorithm?….Pages 420-434
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets….Pages 435-449
A Sweep-Line Method for State Space Exploration….Pages 450-464
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams….Pages 465-479
Simulation Revisited….Pages 480-495
Compositional Message Sequence Charts….Pages 496-511
An Automata Based Interpretation of Live Sequence Charts….Pages 512-527
Coverage Metrics for Temporal Logic Model Checking….Pages 528-542
Parallel Model Checking for the Alternation Free μ-Calculus….Pages 543-558
Model Checking CTL*[DC]….Pages 559-573
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS ….Pages 574-577
The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models….Pages 578-581
The Erlang Verification Tool….Pages 582-585