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, Volume 7

Front Cover
Springer Science & Business Media, Mar 21, 2001 - Computers - 588 pages
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.
 

What people are saying - Write a review

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

Contents

Final Showdown
1
Propositional Reasoning
23
Language Containment Checking with Nondeterministic BDDs
24
Satisfiability Checking Using Boolean Expression Diagrams
39
A Library for Composite Symbolic Representations
52
Synthesis of Linear Ranking Functions
67
Automatic Deductive Verification with Invisible Invariants
82
Incremental Verification by Abstraction
98
An Efficient Iteration Strategy for Symbolic StateSpace Generation
328
Automated Test Generation from Timed Automata
343
Testing an Intentional Naming Scheme Using Genetic Algorithms
358
Problems and Solutions
373
Testing and Analysis Tool for ObjectOriented Software
389
Implementing a Multivalued Symbolic Model Checker
404
Is There a Best Symbolic CycleDetection Algorithm?
420
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets
435

A Technique for Invariant Generation
113
Model Checking Syllabi and Student Carreers
128
Verification of Vortex Workflows
143
Parameterized Verification of Multithreaded Software Libraries
158
Efficient Guiding Towards CostOptimality in UPPAAL
174
Linear Parametric Model Checking of Timed Automata
189
Abstraction in Probabilistic Process Algebra
204
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders
220
HardwareSoftware CoDesign Using Functional Languages
236
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors1
252
Boolean and Cartesian Abstraction for Model Checking C Programs
268
Finding Feasible Counterexamples when Model Checking Abstracted Java Programs
284
The LOOP Compiler for Java and JML
299
Searching Powerset Automata by Combining ExplicitState and Symbolic Model Checking
313
A SweepLine Method for State Space Exploration
450
AssumeGuarantee Based Compositional Reasoning for Synchronous Timing Diagrams
465
Simulation Revisited
480
Compositional Message Sequence Charts
496
An Automata Based Interpretation of Live Sequence Charts
512
Coverage Metrics for Temporal Logic Model Checking
528
Parallel Model Checking for the Alternation Free µCalculus
543
Model Checking CTLDC
559
A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS
574
The ASM Workbench A Tool Environment for ComputerAided Analysis and Validation of Abstract State Machine Models Tool Demonstration
578
The Erlang Verification Tool
582
Author Index
586
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information