Costas Courcoubetis
Proceedings of the Fifth International Conference on Computer Aided Verification
CAV, 1993.

@proceedings{CAV-1993,
	address       = "Elounda, Greece",
	editor        = "Costas Courcoubetis",
	isbn          = "3-540-56922-7",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fifth International Conference on Computer Aided Verification}",
	volume        = 697,
	year          = 1993,
}

Contents (40 items)

16 ×#verification
5 ×#logic
5 ×#model checking
5 ×#realtime
5 ×#using
3 ×#algorithm
3 ×#design
3 ×#performance
3 ×#process
3 ×#source code

CAV-1993-Brayton #design #logic #synthesis #verification

Logic Synthesis and Design Verification (RKB), pp. 1–2.

CAV-1993-HuD #invariant #performance #using #verification

Efficient Verification with BDDs using Implicitly Conjoined Invariants (AJH, DLD), pp. 3–14.

CAV-1993-GuptaF #induction #parametricity #representation #using

Parametric Circuit Representation Using Inductive Boolean Functions (AG, ALF), pp. 15–28.

CAV-1993-BalarinS #approach

An Iterative Approach to Language Containment (FB, ALSV), pp. 29–40.

CAV-1993-HojatiBK #debugging #design #using

BDD-Based Debugging Of Design Using Language Containment and Fair CTL (RH, RKB, RPK), pp. 41–58.

CAV-1993-WolperL #detection #reliability

Reliable Hashing without Collosion Detection (PW, DL), pp. 59–70.

CAV-1993-GrafL #verification

A Tool for Symbolic Program Verification and Abstration (SG, CL), pp. 71–84.

CAV-1993-FernandezKM #equivalence

Symbolic Equivalence Checking (JCF, AK, LM), pp. 85–96.

CAV-1993-KestenMMP #algorithm #logic

A Decision Algorithm for Full Propositional Temporal Logic (YK, ZM, HM, AP), pp. 97–109.

CAV-1993-Krishnakumar #composition #finite #reachability #state machine

Reachability and Recurrence in Extended Finite State Machines: Modular Vector Addition Systems (ASK), pp. 110–122.

CAV-1993-RhoS #automation #generative #invariant #network #verification

Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems (JKR, FS), pp. 123–137.

CAV-1993-KuttyRMDM #concurrent #logic #tool support #verification #visual notation

A Graphical Interval Logic Toolset for Verifying Concurrent Systems (GK, YSR, LEM, LKD, PMMS), pp. 138–153.

CAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification

Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.

CAV-1993-KurshanL #multi #verification

Verification of a Multiplier: 64 Bits and Beyond (RPK, LL), pp. 166–179.

CAV-1993-Varaiya #automation #design #protocol

Protocol Design for an Automated Highway System (PV), p. 180.

CAV-1993-AlurCH #realtime

Computing Accumulated Delays in Real-time Systems (RA, CC, TAH), pp. 181–193.

CAV-1993-MalerP #analysis #multi #reachability

Reachability Analysis of Planar Multi-limear Systems (OM, AP), pp. 194–209.

CAV-1993-YannakakisL #algorithm #performance #realtime

An Efficient Algorithm for Minimizing Real-time Transition Systems (MY, DL), pp. 210–224.

CAV-1993-CourcoubetisDJ #verification

Verification of timing Properties of VHDL (CC, WD, BJ), pp. 225–236.

CAV-1993-LamB #automaton

Alternating RQ Timed Automata (WKCL, RKB), pp. 237–252.

CAV-1993-CeransGL #specification #tool support

Timed Modal Specification — Theory and Tools (KC, JCG, KGL), pp. 253–267.

CAV-1993-Wilding

A Mechanically Verified Application for a Mechanically Verified Environment (MW), pp. 268–279.

CAV-1993-Shankar #realtime #using #verification

Verification of Real-Time Systems Using PVS (NS), pp. 280–291.

CAV-1993-LincolnR #algorithm #consistency #fault #hybrid #interactive #verification

The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model (PL, JMR), pp. 292–304.

CAV-1993-Sogaard-AndersenGGLP #proving #simulation

Computer-Assisted Simulation Proofs (JFSA, SJG, JVG, NAL, AP), pp. 305–319.

CAV-1993-Gordon #imperative #source code #verification

A Verifier and Timing Analyser for Simple Imperative Programs (MJCG), p. 320.

CAV-1993-YonedaSSC #parallel #performance #realtime #verification

Efficient Verification of Parallel Real-Time Systems (TY, AS, BHS, EMC), pp. 321–346.

CAV-1993-Halbwachs #analysis #source code

Delay Analysis in Synchronous Programs (NH), pp. 333–346.

CAV-1993-JourdanMO #realtime #source code #verification

Verifying Quantitative Real-Time Properties of Synchronous Programs (MJ, FM, AO), pp. 347–358.

CAV-1993-HennessyL #logic #message passing #process

A Modal Logic for Message passing Processes (MH, XL), pp. 359–370.

CAV-1993-BrinksmaLB #composition

Functionality Decomposition by Compositional Correstness Preserving Transformation (EB, RL, PB), pp. 371–384.

CAV-1993-EmersonJS #calculus #model checking #on the #μ-calculus

On Model-Checking for Fragments of μ-Calculus (EAE, CSJ, APS), pp. 385–396.

CAV-1993-Valmari #on the fly #set #verification

On-the-Fly Verification with Stubborn Sets (AV), pp. 397–408.

CAV-1993-Peled #model checking #using

All from One, One for All: on Model Checking Using Representatives (DP), pp. 409–423.

CAV-1993-ProbstL #automaton #behaviour #verification

Verifying Timed Behavior Automata with Input/Output Critical Races (DKP, HFL), pp. 424–437.

CAV-1993-GodefroidP #dependence #partial order #verification

Refining Dependencies Improves Partial-Order Verification Methods (PG, DP), pp. 438–449.

CAV-1993-ClarkeFJ #logic #model checking #symmetry

Exploiting Symmetry In Temporal Logic Model Checking (EMC, TF, SJ), pp. 450–462.

CAV-1993-EmersonS #model checking #symmetry

Symmetry and Model Checking (EAE, APS), pp. 463–478.

CAV-1993-DamsGG #generative #modelling

Generation of Reduced Models for Checking Fragments of CTL (DD, OG, RG), pp. 479–490.

CAV-1993-KurshanMOS #process

A Structural Linearization Principle for Processes (RPK, MM, AO, SRS), pp. 491–504.