Gregor von Bochmann, David K. Probst
Proceedings of the Fourth International Workshop on Computer Aided Verification
CAV, 1992.

@proceedings{CAV-1992,
	address       = "Montreal, Canada",
	editor        = "Gregor von Bochmann and David K. Probst",
	isbn          = "3-540-56496-9",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Workshop on Computer Aided Verification}",
	volume        = 663,
	year          = 1992,
}

Contents (32 items)

16 ×#verification
5 ×#model checking
3 ×#case study
3 ×#composition
3 ×#logic
3 ×#performance
3 ×#realtime
3 ×#using
2 ×#behaviour
2 ×#bisimulation

CAV-1992-Lamport #verification

Computer-Hindered Verification (Humans Can Do It Too) (LL), p. 1.

CAV-1992-De-LeonG #abstraction #composition #distributed #realtime #verification

Modular Abstractions for Verifying Real-Time Distributed Systems (HDL, OG), pp. 2–15.

CAV-1992-PoelZ #development #parallel

Layering Techniques for Development of Parallel Systems (MP, JZ), pp. 16–29.

CAV-1992-Larsen #correctness #performance

Efficient Local Correctness Checking (KGL), pp. 30–43.

CAV-1992-EngbergGL #concurrent #verification

Mechanical Verification of Concurrent Systems with TLA (UE, PG, LL), pp. 44–55.

CAV-1992-WrightL #algorithm #concurrent #proving #reasoning #theorem proving #using

Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.

CAV-1992-AagaardL #case study #logic #synthesis #verification

Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification (MA, ML), pp. 69–81.

CAV-1992-HuDDY #specification #verification

Higher-Level Specification and Verification with BDDs (AJH, DLD, AJD, CHY), pp. 82–95.

CAV-1992-BoualiS #bisimulation

Symbolic Bisimulation Minimisation (AB, RdS), pp. 96–108.

CAV-1992-JainKG #scalability #towards #verification

Towards a Verification Technique for Large Synchronous Circuits (PJ, PK, GG), pp. 109–122.

CAV-1992-ProbstL #automaton #behaviour #constraints #verification

Verifying Timed Behavior Automata with Nonbinary Delay Constraints (DKP, HFL), pp. 123–136.

CAV-1992-AlurIKY #approximate #verification

Timing Verification by Successive Approximation (RA, AI, RPK, MY), pp. 137–150.

CAV-1992-BalarinS #verification

A Verification Strategy for Timing-Constrained Systems (FB, ALSV), pp. 151–163.

CAV-1992-McMillan #explosion #problem #using #verification

Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits (KLM), pp. 164–177.

CAV-1992-GodefroidHP #revisited

State-Space Caching Revisited (PG, GJH, DP), pp. 178–191.

CAV-1992-FischerST #algebra #case study #distributed #process #verification

Verification in Process Algebra of the Distributed Control of Track Vehicles — A Case Study (SF, AS, DT), pp. 192–205.

CAV-1992-HamaguchiHY #branch #design #logic #using #verification

Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic (KH, HH, SY), pp. 206–219.

CAV-1992-Bruns #case study #design #safety

A Case Study in Safety-Critical Design (GB), pp. 220–233.

CAV-1992-ShipleCSB #automation #composition #model checking #reduction

Automatic Reduction in CTL Compositional Model Checking (TRS, MC, ALSV, RKB), pp. 234–247.

CAV-1992-Kaivola #composition #linear #logic #model checking

Compositional Model Checking for Linear-Time Temporal Logic (RK), pp. 248–259.

CAV-1992-BensalemBLS #simulation

Property Preserving Simulations (SB, AB, CL, JS), pp. 260–273.

CAV-1992-CourcoubetisDCT #realtime #verification

Verification with Real-Time COSPAN (CC, DLD, MC, PT), pp. 274–287.

CAV-1992-RicoBC #model checking #realtime

Model-Checking for Real-Time Systems Specified in Lotos (NR, GvB, OC), pp. 288–301.

CAV-1992-Cerans #bisimulation #decidability #parallel #process

Decidability of Bisimulation Equivalences for Parallel Timer Processes (KC), pp. 302–315.

CAV-1992-Bradfield #model checking #proving

A Proof Assistant for Symbolic Model-Checking (JCB), pp. 316–329.

CAV-1992-Mader

Tableau Recycling (AM), pp. 330–342.

CAV-1992-MeryM #ide #interactive #named #specification #verification

Crocos: An Integrated Environment for Interactive Verification of SDL Specifications (DM, AM), pp. 343–356.

CAV-1992-Corbett #integer #liveness #programming #safety #verification

Verifying General Safety and Liveness Propterties with Integer Programming (JCC), pp. 357–369.

CAV-1992-CelikkanC #behaviour #generative

Generating Diagnostic Information for Behavioral Preorders (UC, RC), pp. 370–383.

CAV-1992-HiguchiSSFK #communication #finite #invariant #state machine #verification

A Verification Procedure via Invariant for Extended Communicating Finite-State Machines (MH, OS, HS, MF, TK), pp. 384–395.

CAV-1992-HojatiTKB #performance #regular expression

Efficient ω-Regular Language Containment (RH, HJT, RPK, RKB), pp. 396–409.

CAV-1992-CleavelandKS #calculus #model checking #performance #μ-calculus

Faster Model Checking for the Modal μ-Calculus (RC, MK, BS), pp. 410–422.