default search action
4th CAV 1992: Montreal, Canada
- Gregor von Bochmann, David K. Probst:
Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings. Lecture Notes in Computer Science 663, Springer 1993, ISBN 3-540-56496-9
Invited Lecture
- Leslie Lamport:
Computer-Hindered Verification (Humans Can Do It Too). 1
Session: Reduction Techniques 1
- Hana De-Leon, Orna Grumberg:
Modular Abstractions for Verifying Real-Time Distributed Systems. 2-15 - Mannes Poel, Job Zwiers:
Layering Techniques for Development of Parallel Systems. 16-29 - Kim Guldstrand Larsen:
Efficient Local Correctness Checking. 30-43
Session: Proof Checking
- Urban Engberg, Peter Grønning, Leslie Lamport:
Mechanical Verification of Concurrent Systems with TLA. 44-55 - Joakim von Wright, Thomas Långbacka:
Using a Theorem Prover for Reasoning about Concurrent Algorithms. 56-68 - Mark D. Aagaard, Miriam Leeser:
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. 69-81
Session: Symbolic Verification 1
- Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang:
Higher-Level Specification and Verification with BDDs. 82-95 - Amar Bouali, Robert de Simone:
Symbolic Bisimulation Minimisation. 96-108 - Prabhat Jain, Prabhakar Kudva, Ganesh Gopalakrishnan:
Towards a Verification Technique for Large Synchronous Circuits. 109-122
Session: Timing Verification 1
- David K. Probst, Hon Fung Li:
Verifying Timed Behavior Automata with Nonbinary Delay Constraints. 123-136 - Rajeev Alur, Alon Itai, Robert P. Kurshan, Mihalis Yannakakis:
Timing Verification by Successive Approximation. 137-150 - Felice Balarin, Alberto L. Sangiovanni-Vincentelli:
A Verification Strategy for Timing-Constrained Systems. 151-163
Session: Partial-Order Approaches
- Kenneth L. McMillan:
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. 164-177 - Patrice Godefroid, Gerard J. Holzmann, Didier Pirottin:
State-Space Caching Revisited. 178-191
Session: Case Studies
- Siegfried Fischer, Andreas Scholz, Dirk Taubner:
Verification in Process Algebra of the Distributed Control of Track Vehicles - A Case Study. 192-205 - Kiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima:
Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic. 206-219 - Glenn Bruns:
A Case Study in Safety-Critical Design. 220-233
Session: Reduction Techniques 2
- Thomas R. Shiple, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli, Robert K. Brayton:
Automatic Reduction in CTL Compositional Model Checking. 234-247 - Roope Kaivola:
Compositional Model Checking for Linear-Time Temporal Logic. 248-259 - Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis:
Property Preserving Simulations. 260-273
Session: Timing Verification 2
- Costas Courcoubetis, David L. Dill, Magda Chatzaki, Panagiotis Tzounakis
:
Verification with Real-Time COSPAN. 274-287 - Nathalie Rico, Gregor von Bochmann, Omar Cherkaoui:
Model-Checking for Real-Time Systems Specified in Lotos. 288-301 - Karlis Cerans:
Decidability of Bisimulation Equivalences for Parallel Timer Processes. 302-315
Session: Model and Proof Checking
- Julian C. Bradfield:
A Proof Assistant for Symbolic Model-Checking. 316-329 - Angelika Mader
Tableau Recycling. 330-342 - Dominique Méry, Abdelillah Mokkedem:
Crocos: An Integrated Environment for Interactive Verification of SDL Specifications. 343-356
Session: Other Approaches
- James C. Corbett:
Verifying General Safety and Liveness Propterties with Integer Programming. 357-369 - Ufuk Celikkan, Rance Cleaveland:
Generating Diagnostic Information for Behavioral Preorders. 370-383 - Masahiro Higuchi, Osamu Shirakawa, Hiroyuki Seki, Mamoru Fujii, Tadao Kasami:
A Verification Procedure via Invariant for Extended Communicating Finite-State Machines. 384-395
Session: Symbolic Verification 2
- Ramin Hojati, Hervé J. Touati, Robert P. Kurshan, Robert K. Brayton:
Efficient omega-Regular Language Containment. 396-409 - Rance Cleaveland, Marion Klein, Bernhard Steffen:
Faster Model Checking for the Modal Mu-Calculus. 410-422
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-22 18:47 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: