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
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
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
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
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.
last updated on 2024-12-16 22:15 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: