Computer Aided Verification: 7th International Conference, CAV ’95 Liège, Belgium, July 3–5, 1995 Proceedings

Randal E. Bryant (auth.), Pierre Wolper (eds.)3540600450, 9783540600459

This volume constitutes the proceedings of the 7th International Conference on Computer Aided Verification, CAV ’95, held in Liège, Belgium in July 1995.
The book contains the 31 refereed full research papers selected for presentation at CAV ’95 as well as abstracts or full papers of the three invited presentations. Originally oriented towards finite-state concurrent systems, CAV now covers all styles of verification approaches and a variety of application areas. The papers included range from theoretical issues to concrete applications with a certain emphasis on verification tools and the algorithms and techniques needed for their implementations. Beyond finite-state systems, real-time systems and hybrid systems are an important part of the conference.

---

Table of contents :
Multipliers and dividers: Insights on arithmetic circuit verification (extended abstract)….Pages 1-3
Global rebuilding of OBDDs avoiding memory requirement maxima….Pages 4-15
Generating BDD models for process algebra terms….Pages 16-30
Hardware verification using monadic second-order logic….Pages 31-41
Verifying safety properties of a class of infinite-state distributed algorithms….Pages 42-53
Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving….Pages 54-69
CAVEAT: technique and tool for computer aided verification and transformation….Pages 70-83
An integration of model checking with automated proof checking….Pages 84-97
Automatic datapath abstraction in hardware systems….Pages 98-113
Toupie=μ-calculus+constraints….Pages 114-126
Safety property verification of Esterel programs and applications to telecommunications software….Pages 127-140
Methods for Mu-calculus model checking: A tutorial….Pages 141-141
Efficient checking of behavioural relations and modal assertions using fixed-point inversion….Pages 142-154
It usually works: The temporal logic of stochastic systems….Pages 155-165
Local liveness for compositional modeling of fair reactive systems….Pages 166-179
Trace theoretic verification of asynchronous circuits using unfoldings….Pages 180-195
From duration calculus to linear hybrid automata….Pages 196-210
Local model checking for real-time systems….Pages 211-224
Algorithmic analysis of nonlinear hybrid systems….Pages 225-238
On polynomial-size programs winning finite-state games….Pages 239-252
The rabin index and chain automata, with applications to automata and games….Pages 253-266
An automata-theoretic approach to fair realizability and synthesis….Pages 267-278
Supervisory control of finite state machines….Pages 279-292
Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form….Pages 293-308
Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach….Pages 309-324
Augmenting branching temporal logics with existential quantification over atomic propositions….Pages 325-338
Modelling asynchrony with a synchronous model….Pages 339-352
On the model checking problem for branching time logics and basic parallel processes….Pages 353-366
Using formal verification/analysis methods on the critical path in system design: A case study….Pages 367-380
Automated analysis of an audio control protocol….Pages 381-394
Interactively verifying a simple real-time scheduler….Pages 395-408
Verification of real-time systems by successive over and under approximation….Pages 409-422
Efficient timing analysis of a class of Petri nets….Pages 423-436
Verifying ω-regular properties for a subclass of linear hybrid systems….Pages 437-450