


default search action
3rd CAV 1991: Aalborg, Denmark
- Kim Guldstrand Larsen, Arne Skou:

Computer Aided Verification, 3rd International Workshop, CAV '91, Aalborg, Denmark, July, 1-4, 1991, Proceedings. Lecture Notes in Computer Science 575, Springer 1992, ISBN 3-540-55179-4
Session 1: Equivalence Checking
- Colin Sterling:

Taming Infinite State Spaces. 1 - Hans Hüttel

:
Silence is Golden: Branching Bisimilarity is Decidable for Context-Free Processes. 2-12 - Henri Korver:

Computing Distinguishing Formulas for Branching Bisimulation. 13-23
Session 2: Model Checking
- Henrik Reif Andersen, Glynn Winskel:

Compositional Checking of Satisfaction. 24-36 - Rocco De Nicola, Alessandro Fantechi, Stefania Gnesi, Gioia Ristori:

An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems. 37-47 - Rance Cleaveland, Bernhard Steffen:

A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. 48-58
Session 3: Applications 1
- A. Prasad Sistla, Lenore D. Zuck:

Automatic Temporal Verification of Buffer Systems. 59-69 - William R. Bevier, Jørgen F. Søgaard-Andersen:

Mechanically Checked Proofs of Kernel Specification. 70-82 - Stein Gjessing, Stein Krogdahl, Ellen Munthe-Kaas:

A Top Down Approach to the Formal Specification of SCI Cache Coherence. 83-91
Session 4: Applications 2
- George S. Avrunin, Ugo A. Buy, James C. Corbett:

Integer Programming in the Analysis of Concurrent Systems. 92-102 - Michel Barbeau

, Gregor von Bochmann:
The Lotos Model of a Fault Protected System and its Verification Using a Petri Net Based Approach. 103-113 - Anne Rasse:

Error Diagnosis in Finite Communicating Systems. 114-124 - Ranga Vemuri

, Anuradha Sridhar:
Temporal Precondition Verification of Design Transformations. 125-135
Session 5: Tools for Process Algebras
- Huimin Lin:

PAM: A Process Algebra Manipulator. 136-146 - Claus Torp Jensen:

The Concurrency Workbench with Priorities. 147-157 - Sjouke Mauw

, Gert J. Veltink:
A Proof Assistant for PSF. 158-168
Session 6: The State Explosion Problem
- Alain Finkel, Laure Petrucci:

Avoiding State Exposion by Composition of Minimal Covering Graphs. 169-180 - Jean-Claude Fernandez, Laurent Mounier:

"On the Fly" Verification of Behavioural Equivalences and Preorders. 181-191 - Claude Jard, Thierry Jéron

:
Bounded-memory Algorithms for Verification On-the-fly. 192-202
Session 7: Symbolic Model Checking
- Reinhard Enders, Thomas Filkorn, Dirk Taubner:

Generating BDDs for Symbolic Model Checking in CCS. 203-213 - Hiromi Hiraishi, Kiyoharu Hamaguchi, Hiroyuki Ochi, Shuzo Yajima:

Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification. 214-224 - Thomas Filkorn:

Functional Extension of Symbolic Model Checking. 225-232
Session 8: Verification and Transformation Techniques
- Wenbo Mao, George J. Milne

:
An Automated Proof Technique for Finite-State Machine Equivalence. 233-243 - Ed Brinksma:

From Data Structure to Process Structure. 244-254 - David L. Dill, Alan J. Hu, Howard Wong-Toi:

Checking for Language Inclusion Using Simulation Preorders. 255-265 - Nicoletta De Francesco, Paola Inverardi:

A Semantic Driven Method to Check the Finiteness of CCS Processes. 266-276
Session 9: Higher Order Logic
- Matthias Mutz:

Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior. 277-287 - Monica Nesi:

Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic. 288-298 - Carl-Johan H. Seger, Jeffrey J. Joyce:

A Two-Level Formal Verification Methodology using HOL and COSMOS. 299-309 - Linda Christoff, Ivan Christoff:

Efficient Algorithms for Verification of Equivalences for Probabilistic Processes. 310-321
Session 10: Partial Order Approaches
- David K. Probst, Hon Fung Li:

Partial-Order Model Checking: A Guide for the Perplexed. 322-331 - Patrice Godefroid, Pierre Wolper

:
Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. 332-342 - Joan Feigenbaum, Jeremy A. Kahn, Carsten Lund:

Complexity Results for POMSET Languages. 343-353
Session 11: Hardware Verification
- David M. Goldschlag:

Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits. 354-364 - Klaus Schneider

, Ramayya Kumar, Thomas Kropf
:
Automating Most Parts of Hardware Proofs in HOL. 365-375
Session 13: Timed Specification and Verification 1
- Xavier Nicollin, Joseph Sifakis:

An Overview and Synthesis on Timed Process Algebras. 376-398 - Costas Courcoubetis:

Minimum and Maximum Delay Problems in Real-Time Systems. 399-409 - Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima:

Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic. 410-420
Session 14: Timed Specification and Verification 2
- Armen Gabrielian, R. Iyer:

Verifying Properties of HMS Machine Specifications of Real-Time Systems. 421-431 - Alan Jeffrey:

A Linear Time Process Algebra. 432-442 - Uno Holmer, Kim Guldstrand Larsen, Wang Yi:

Deciding Properties of Regular Real Time Processes. 443-453
Session 15: Automata
- Costas Courcoubetis, Susanne Graf, Joseph Sifakis:

An Algebra of Boolean Processes. 454-465 - Michel Langevin, Eduard Cerny:

Comparing Generic State Machines. 466-476 - Gjalt G. de Jong:

An Automata Theoretic Approach to Temporal Logic. 477-487

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














