## 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 7This 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 |

586 | |

### Other editions - View all

Tools and Algorithms for the Construction and Analysis of Systems ..., Volume 7 TACAS 2001 No preview available - 2001 |

Tools and Algorithms for the Construction and Analysis of Systems: 7th ... Tiziana Margaria,Wang Yi No preview available - 2014 |

### Common terms and phrases

abstraction algorithm analysis ape graph applied approach automata automaton binary decision diagrams bisimulation checker clock components Computer Science conﬁguration constraint construction contains counter-example deﬁned deﬁnition denote diagrams E.M. Clarke efﬁcient encoding equivalence class example execution expression ﬁnd ﬁnite ﬁrst Formal formal verification formula function IEEE implementation inﬁnite initial input integer invariant iterations Java Kripke structure labeled language Lecture Notes linear LNCS LOOP memory model checking module node Notes in Computer operator OWCTY parameter partition path predicate probabilistic problem Proc process algebra processor progress measure properties protocol reachable represented Rockall SAFL satisﬁes semantics sequence simulation space speciﬁcation Springer-Verlag stack machine strongly connected components structure sweep-line method symbolic model checking TACAS techniques temporal logic Theorem tion tool transition relation transition system trivectors tuple variables vector veriﬁcation