Kim Guldstrand Larsen, Arne Skou
Proceedings of the Third International Workshop on Computer Aided Verification
CAV, 1991.

@proceedings{CAV-1991,
	address       = "Aalborg, Denmark",
	editor        = "Kim Guldstrand Larsen and Arne Skou",
	isbn          = "3-540-55179-4",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Third International Workshop on Computer Aided Verification}",
	volume        = 575,
	year          = 1991,
}

Contents (44 items)

13 ×#verification
10 ×#process
6 ×#model checking
6 ×#proving
6 ×#using
5 ×#logic
4 ×#algebra
4 ×#concurrent
4 ×#specification
3 ×#algorithm

CAV-1991-Sterling #infinity

Taming Infinite State Spaces (CS), p. 1.

CAV-1991-Huttel #branch #decidability #process #similarity

Silence is Golden: Branching Bisimilarity is Decidable for Context-Free Processes (HH), pp. 2–12.

CAV-1991-Korver #bisimulation #branch

Computing Distinguishing Formulas for Branching Bisimulation (HK), pp. 13–23.

CAV-1991-AndersenW #composition

Compositional Checking of Satisfaction (HRA, GW), pp. 24–36.

CAV-1991-NicolaFGR #behaviour #concurrent #framework #logic #verification

An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems (RDN, AF, SG, GR), pp. 37–47.

CAV-1991-CleavelandS #algorithm #calculus #linear #model checking #μ-calculus

A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal μ-Calculus (RC, BS), pp. 48–58.

CAV-1991-Sistla #automation #verification

Automatic Temporal Verification of Buffer Systems (APS, LDZ), pp. 59–69.

CAV-1991-BevierS #kernel #proving #specification

Mechanically Checked Proofs of Kernel Specification (WRB, JFSA), pp. 70–82.

CAV-1991-GjessingKM #approach #specification #top-down

A Top Down Approach to the Formal Specification of SCI Cache Coherence (SG, SK, EMK), pp. 83–91.

CAV-1991-AvruninBC #analysis #concurrent #integer #programming

Integer Programming in the Analysis of Concurrent Systems (GSA, UAB, JCC), pp. 92–102.

CAV-1991-BarbeauB #approach #fault #petri net #using #verification

The Lotos Model of a Fault Protected System and its Verification Using a Petri Net Based Approach (MB, GvB), pp. 103–113.

CAV-1991-Rasse #communication #fault #finite

Error Diagnosis in Finite Communicating Systems (AR), pp. 114–124.

CAV-1991-VemuriS #design #verification

Temporal Precondition Verification of Design Transformations (RV, AS), pp. 125–135.

CAV-1991-Lin #algebra #named #process

PAM: A Process Algebra Manipulator (HL), pp. 136–146.

CAV-1991-Jensen #concurrent

The Concurrency Workbench with Priorities (CTJ), pp. 147–157.

CAV-1991-MauwV #proving

A Proof Assistant for PSF (SM, GJV), pp. 158–168.

CAV-1991-FinkelP #composition #graph

Avoiding State Exposion by Composition of Minimal Covering Graphs (AF, LP), pp. 169–180.

CAV-1991-FernandezM #behaviour #on the fly #verification

“On the Fly” Verification of Behavioural Equivalences and Preorders (JCF, LM), pp. 181–191.

CAV-1991-JardJ #algorithm #bound #on the fly #verification

Bounded-memory Algorithms for Verification On-the-fly (CJ, TJ), pp. 192–202.

CAV-1991-EndersFT #generative #model checking

Generating BDDs for Symbolic Model Checking in CCS (RE, TF, DT), pp. 203–213.

CAV-1991-HiraishiHOY #logic #model checking #verification

Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification (HH, KH, HO, SY), pp. 214–224.

CAV-1991-Filkorn #functional #model checking

Functional Extension of Symbolic Model Checking (TF), pp. 225–232.

CAV-1991-MaoM #automation #equivalence #finite #proving #state machine

An Automated Proof Technique for Finite-State Machine Equivalence (WM, GJM), pp. 233–243.

CAV-1991-Brinksma #data type #process

From Data Structure to Process Structure (EB), pp. 244–254.

CAV-1991-DillHW #simulation #using

Checking for Language Inclusion Using Simulation Preorders (DLD, AJH, HWT), pp. 255–265.

CAV-1991-FrancescoI #process #semantics

A Semantic Driven Method to Check the Finiteness of CCS Processes (NDF, PI), pp. 266–276.

CAV-1991-Mutz #behaviour #correctness #proving #term rewriting #using

Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior (MM), pp. 277–287.

CAV-1991-Nesi #higher-order #induction #logic #process #proving #specification

Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic (MN), pp. 288–298.

CAV-1991-SegerJ #using #verification

A Two-Level Formal Verification Methodology using HOL and COSMOS (CJHS, JJJ), pp. 299–309.

CAV-1991-ChristoffC #algorithm #performance #probability #process #verification

Efficient Algorithms for Verification of Equivalences for Probabilistic Processes (LC, IC), pp. 310–321.

CAV-1991-ProbstL #model checking #partial order

Partial-Order Model Checking: A Guide for the Perplexed (DKP, HFL), pp. 322–331.

CAV-1991-GodefroidW #concurrent #partial order #performance #safety #using #verification

Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties (PG, PW), pp. 332–342.

CAV-1991-FeigenbaumKL #complexity

Complexity Results for POMSET Languages (JF, JAK, CL), pp. 343–353.

CAV-1991-Goldschlag #liveness #safety #verification

Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits (DMG), pp. 354–364.

CAV-1991-SchneiderKK #automation #hardware #proving

Automating Most Parts of Hardware Proofs in HOL (KS, RK, TK), pp. 365–375.

CAV-1991-NicollinS #algebra #overview #process #synthesis

An Overview and Synthesis on Timed Process Algebras (XN, JS), pp. 376–398.

CAV-1991-Courcoubetis #problem #realtime

Minimum and Maximum Delay Problems in Real-Time Systems (CC), pp. 399–409.

CAV-1991-HamaguchiHY #branch #logic #model checking #using #verification

Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic (KH, HH, SY), pp. 410–420.

CAV-1991-GabrielianI #realtime #specification #verification

Verifying Properties of HMS Machine Specifications of Real-Time Systems (AG, RI), pp. 421–431.

CAV-1991-Jeffrey #algebra #linear #process

A Linear Time Process Algebra (AJ), pp. 432–442.

CAV-1991-HolmerLY #process #realtime

Deciding Properties of Regular Real Time Processes (UH, KGL, WY), pp. 443–453.

CAV-1991-CourcoubetisGS #algebra #process

An Algebra of Boolean Processes (CC, SG, JS), pp. 454–465.

CAV-1991-LangevinC #state machine

Comparing Generic State Machines (ML, EC), pp. 466–476.

CAV-1991-Jong #approach #automaton #logic

An Automata Theoretic Approach to Temporal Logic (GGdJ), pp. 477–487.