Rajeev Alur, Thomas A. Henzinger
Proceedings of the Eighth International Conference on Computer Aided Verification
CAV, 1996.

@proceedings{CAV-1996,
	address       = "New Brunswick, New Jersey, USA",
	editor        = "Rajeev Alur and Thomas A. Henzinger",
	isbn          = "3-540-61474-5",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Eighth International Conference on Computer Aided Verification}",
	volume        = 1102,
	year          = 1996,
}

Contents (51 items)

29 ×#verification
8 ×#model checking
7 ×#named
6 ×#using
5 ×#automation
5 ×#protocol
4 ×#algorithm
4 ×#analysis
4 ×#tool support
3 ×#concurrent

CAV-1996-BoigelotG #communication #infinity #protocol #using #verification

Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (BB, PG), pp. 1–12.

CAV-1996-McMillan #model checking #representation

A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking (KLM), pp. 13–25.

CAV-1996-Avrunin #algebra #geometry #model checking #using

Symbolic Model Checking Using Algebraic Geometry (GSA), pp. 26–37.

CAV-1996-PistoreS #algorithm #refinement #π-calculus

A Partition Refinement Algorithm for the π-Calculus (MP, DS), pp. 38–49.

CAV-1996-Baier #algorithm #bisimulation #polynomial #probability #simulation #testing

Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation (CB), pp. 50–61.

CAV-1996-Walukiewicz #automaton #game studies #model checking #process

Pushdown Processes: Games and Model Checking (IW), pp. 62–74.

CAV-1996-KupfermanV

Module Checking (OK, MYV), pp. 75–86.

CAV-1996-EmersonN #automation #verification

Automatic Verification of Parameterized Synchronous Systems (EAE, KSN), pp. 87–98.

CAV-1996-ShuklaHR #game studies #model checking #verification

HORNSAT, Model Checking, Verification and games (SKS, HBHI, DJR), pp. 99–110.

CAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification

Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.

CAV-1996-RuessSS #composition #verification

Modular Verification of SRT Division (HR, NS, MKS), pp. 123–134.

CAV-1996-KapurS #multi #product line #verification

Mechanically Verifying a Family of Multiplier Circuits (DK, MS), pp. 135–146.

CAV-1996-IpD #component #verification

Verifying Systems with Replicated Components in Murphi (CNI, DLD), pp. 147–158.

CAV-1996-Fujita #verification

Verification of Arithmetic Circuits by Comparing Two Similar Circuits (MF), pp. 159–168.

CAV-1996-Rushby #automation #deduction #formal method

Automated Deduction and Formal Methods (JMR), pp. 169–183.

CAV-1996-PnueliS #algorithm #deduction #framework #platform #verification

A Platform for Combining Deductive with Algorithmic Verification (AP, ES), pp. 184–195.

CAV-1996-GrafS #invariant #proving #theorem proving #using #verification

Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.

CAV-1996-SipmaUM #deduction #model checking

Deductive Model Checking (HS, TEU, ZM), pp. 208–219.

CAV-1996-BerregebBR #automation #commutative #induction #verification

Automated Verification by Induction with Associative-Commutative Operators (NB, AB, MR), pp. 220–231.

CAV-1996-TripakisY #analysis #bisimulation

Analysis of Timed Systems Based on Time-Abstracting Bisimulation (ST, SY), pp. 232–243.

CAV-1996-BengtssonGKLLPY #protocol #using #verification

Verification of an Audio Protocol with Bus Collision Using UPPAAL (JB, WODG, KJK, KGL, FL, PP, WY), pp. 244–256.

CAV-1996-CamposG #analysis #model checking #verification

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (SVAC, OG), pp. 257–268.

CAV-1996-AzizSSB #markov #verification

Verifying Continuous Time Markov Chains (AA, KS, VS, RKB), pp. 269–276.

CAV-1996-Greenstreet #difference #equation #safety #verification

Verifying Safety Properties of Differential Equations (MRG), pp. 277–287.

CAV-1996-AlfaroM #diagrams #verification

Temporal Verification by Diagram Transformations (LdA, ZM), pp. 288–299.

CAV-1996-ParkD #distributed #protocol #transaction #verification

Protocol Verification by Aggregation of Distributed Transactions (SP, DLD), pp. 300–310.

CAV-1996-Gribomont #reduction #refinement #theorem

Atomicity Refinement and Trace Reduction Theorems (EPG), pp. 311–322.

CAV-1996-BensalemLS #automation #generative #invariant

Powerful Techniques for the Automatic Generation of Invariants (SB, YL, HS), pp. 323–335.

CAV-1996-MillerK

Saving Space by Fully Exploiting Invisible Transitions (HM, SK), pp. 336–347.

CAV-1996-FernandezJJV #generative #on the fly #testing #using #verification

Using On-The-Fly Verification Techniques for the Generation of test Suites (JCF, CJ, TJ, CV), pp. 348–359.

CAV-1996-NelkenF #automation #natural language #specification

Automatic Translation of Natural Language System Specifications (RN, NF), pp. 360–371.

CAV-1996-KupfermanV96a #verification

Verification of Fair Transisiton Systems (OK, MYV), pp. 372–382.

CAV-1996-HolzmannP

The State of SPIN (GJH, DP), pp. 385–389.

CAV-1996-Dill #verification

The Murphi Verification System (DLD), pp. 390–393.

CAV-1996-CleavelandS #concurrent

The NCSU Concurrency Workbench (RC, SS), pp. 394–397.

CAV-1996-CleavelandLSS #concurrent #development

The Concurrency Factory: A Development Environment for Concurrent Systems (RC, PML, SAS, OS), pp. 398–401.

CAV-1996-ClarkeBLXS #analysis #bound #named #realtime #specification #tool support #visual notation

XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Sytems (DC, HBA, IL, HlX, OS), pp. 402–405.

CAV-1996-MerinoT #analysis #communication #integration #named #protocol #verification

EVP: Integration of FDTs for the Analysis and Verification of Communication Protocols (PM, JMT), pp. 406–410.

CAV-1996-OwreRRSS #model checking #named #proving #specification

PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.

CAV-1996-BjornerBCCKMSU #named #realtime #verification

STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems (NB, AB, EYC, MC, AK, ZM, HS, TEU), pp. 415–418.

CAV-1996-ClarkeMCH #model checking

Symbolic Model Checking (EMC, KLM, SVAC, VHG), pp. 419–427.

CAV-1996-BraytonHSSACEKKPQRSSSV #named #synthesis #verification

VIS: A System for Verification and Synthesis (RKB, GDH, ALSV, FS, AA, STC, SAE, SPK, YK, AP, SQ, RKR, SS, TRS, GS, TV), pp. 428–432.

CAV-1996-AnonBCCLSTXZ #design #tool support #verification

MDG Tools for the Verification of RTL Designs (KDA, NB, EC, FC, ML, XS, ST, YX, ZZ), pp. 433–436.

CAV-1996-FernandezGKMMS #named #protocol #validation #verification

CADP — A Protocol Validation and Verification Toolbox (JCF, HG, AK, LM, RM, MS), pp. 437–440.

CAV-1996-BoualiRRS #set #tool support

The FC2TOOLS Set (AB, AR, VR, RdS), pp. 441–445.

CAV-1996-MoserMRKD #logic #realtime #tool support #visual notation

The Real-Time Graphical Interval Logic Toolset (LEM, PMMS, YSR, GK, LKD), pp. 446–449.

CAV-1996-SteffenMCB

The METAFrame’95 Environment (BS, TMS, AC, VB), pp. 450–453.

CAV-1996-KochUW #verification

Verification Support Environment (FAK, MU, SW), pp. 454–457.

CAV-1996-AmbroiseR #named #simulation #verification

Marella: A Tool for Simulation and Verification (DA, BR), pp. 458–461.

CAV-1996-Gonthier #concurrent #garbage collection #safety #verification

Verifying the Safety of a Practical Concurrent Garbage Collector (GG), pp. 462–465.

CAV-1996-CapellmannDFGNO #abstraction #behaviour #case study #detection #interactive #network #verification

Verification by Behaviour Abstraction — A Case Study of Service Interaction Detection in Intelligent Telephone Networks (CC, RD, FFV, RGE, UN, PO), pp. 466–469.