Edmund M. Clarke, Robert P. Kurshan
Proceedings of the Second International Workshop on Computer Aided Verification
CAV, 1990.

@proceedings{CAV-1990,
	address       = "New Brunswick, New Jersey, USA",
	editor        = "Edmund M. Clarke and Robert P. Kurshan",
	isbn          = "3-540-54477-1",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Second International Workshop on Computer Aided Verification}",
	volume        = 531,
	year          = 1990,
}

Contents (38 items)

13 ×#verification
8 ×#using
5 ×#logic
4 ×#automation
4 ×#model checking
3 ×#algebra
3 ×#composition
3 ×#explosion
3 ×#problem
3 ×#protocol

CAV-1990-Clarke #explosion #logic #model checking #problem

Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem (EMC), p. 1.

CAV-1990-Eveking #automation #hardware #verification

Automatic Verification of Extensions of Hardware Descriptions (HE), pp. 2–12.

CAV-1990-BerthelotJP #analysis #named #petri net

PAPETRI: Environment for the Analysis of Petri Nets (GB, CJ, LP), pp. 13–22.

CAV-1990-CoudertMB #diagrams #verification

Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams (OC, JCM, CB), pp. 23–32.

CAV-1990-BryantS #modelling #using #verification

Formal Verification of Digital Circuits Using Symbolic Ternary System Models (REB, CJHS), pp. 33–43.

CAV-1990-HiraishiMH #logic #model checking

Vectorized Model Checking for Computation Tree Logic (HH, SM, KH), pp. 44–53.

CAV-1990-Pixley #equivalence #hardware #implementation

Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence (CP), pp. 54–64.

CAV-1990-RoyS

Auto/Autograph (VR, RdS), pp. 65–75.

CAV-1990-NakamuraKFT #logic #using #verification

A Data Path Verifier for Register Transfer Level Using Temporal Logic Language Tokio (HN, YK, MF, HT), pp. 76–85.

CAV-1990-CamuratiGPR #model checking #using

The Use of Model Checking in ATPG for Sequential Circuits (PC, MG, PP, MSR), pp. 86–95.

CAV-1990-LloretAV #communication #composition #design #petri net #protocol #using #verification

Compositional Design and Verification of Communication Protocols, Using Labelled Petri Nets (JCL, PA, FV), pp. 96–105.

CAV-1990-Ness #analysis

Issues Arising in the Analysis of L.0 (LAN), pp. 106–115.

CAV-1990-Langevin #automation #calculus #verification

Automated RTL Verification Based on Predicate Calculus (ML), pp. 116–125.

CAV-1990-LaiPD #on the #protocol #using #verification

On Using Protean To Verify ISO FTAM Protocol (RL, KRP, TSD), pp. 126–135.

CAV-1990-EmersonMSS #reasoning

Quantitative Temporal Reasoning (EAE, AKM, APS, JS), pp. 136–145.

CAV-1990-ProbstL #explosion #partial order #problem #semantics #using

Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous Systems (DKP, HFL), pp. 146–155.

CAV-1990-Valmari #explosion

A Stubborn Attack On State Explosion (AV), pp. 156–165.

CAV-1990-JanickiK #graph #reachability #simulation #using

Using Optimal Simulations to Reduce Reachability Graphs (RJ, MK), pp. 166–175.

CAV-1990-Godefroid #automation #partial order #using #verification

Using Partial Orders to Improve Automatic Verification Methods (PG), pp. 176–185.

CAV-1990-GrafS #composition #finite

Compositional Minimization of Finite State Systems (SG, BS), pp. 186–196.

CAV-1990-BouajjaniFH #generative

Minimal Model Generation (AB, JCF, NH), pp. 197–203.

CAV-1990-Josko #equivalence

A Context Dependent Equivalence Relation Between Kripke Structures (BJ), pp. 204–213.

CAV-1990-ShurekG #composition #framework #verification

The Modular Framework of Computer-Aided Verification (GS, OG), pp. 214–223.

CAV-1990-Burch #liveness #safety #verification

Verifying Liveness Properties by Verifying Safety Properties (JRB), pp. 224–232.

CAV-1990-CourcoubetisVWY #algorithm #memory management #performance #verification

Memory Efficient Algorithms for the Verification of Temporal Properties (CC, MYV, PW, MY), pp. 233–242.

CAV-1990-PengP #approach #communication #concurrent #detection #finite #network #problem #state machine

A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines (WP, SP), pp. 243–252.

CAV-1990-HamaguchiHY #branch #complexity #linear #logic #model checking

Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity (KH, HH, SY), pp. 253–262.

CAV-1990-Yodaiken #algebra #automaton #feedback

The Algebraic Feedback Product of Automata (VY), pp. 263–271.

CAV-1990-Wong-ToiD #process #specification

Synthesizing Processes and Schedulers from Temporal Specifications (HWT, DLD), pp. 272–281.

CAV-1990-GolaszewskiK

Task-Driven Supervisory Control of Discrete Event Systems (CHG, RPK), pp. 282–291.

CAV-1990-BuyM #liveness #proving

A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers (UAB, RM), pp. 292–301.

CAV-1990-LoewensteinD #higher-order #logic #multi #protocol #simulation #using #verification

Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic (PL, DLD), pp. 302–311.

CAV-1990-CarringtonR #refinement

Computer Assistance for Program Refinement (DAC, KAR), pp. 312–321.

CAV-1990-MorrisH #execution #symbolic computation #verification

Program Verification by Symbolic Execution of Hyperfinite Ideal Machines (JMM, MH), pp. 322–332.

CAV-1990-BarbeauB #specification

Extension of the Karp and Miller Procedure to Lotos Specifications (MB, GvB), pp. 333–342.

CAV-1990-JosephsU #algebra

An Algebra for Delay-Insensitive Circuits (MBJ, JTU), pp. 343–352.

CAV-1990-MadelaineV #algebra #automaton #process

Finiteness Conditions and Structural Construction of Automata for All Process Algebras (EM, DV), pp. 353–363.

CAV-1990-Cleaveland #automation #bisimulation #on the

On Automatically Explaining Bisimulation Inequivalence (RC), pp. 364–372.