Pierre Wolper
Proceedings of the Seventh International Conference on Computer Aided Verification
CAV, 1995.

@proceedings{CAV-1995,
	address       = "Liège, Belgium",
	editor        = "Pierre Wolper",
	isbn          = "3-540-60045-0",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Seventh International Conference on Computer Aided Verification}",
	volume        = 939,
	year          = 1995,
}

Contents (34 items)

10 ×#verification
6 ×#model checking
5 ×#using
4 ×#analysis
4 ×#logic
3 ×#automation
3 ×#calculus
3 ×#game studies
3 ×#hybrid
3 ×#modelling

CAV-1995-Bryant #multi #verification

Multipliers and Dividers: Insights on Arithmetic Circuits Verification (REB), pp. 1–3.

CAV-1995-BernMS #memory management

Global rebuilding of OBDDs Avoiding Memory Requirement Maxima (JB, CM, AS), pp. 4–15.

CAV-1995-DsouzaB #algebra #generative #modelling #process

Generating BDD Models for Process Algebra Terms (AD, BB), pp. 16–30.

CAV-1995-BasinK #hardware #higher-order #logic #monad #using #verification

Hardware Verification using Monadic Second-Order Logic (DAB, NK), pp. 31–41.

CAV-1995-JonssonK #algorithm #distributed #infinity #safety #verification

Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms (BJ, LK), pp. 42–53.

CAV-1995-DingelF #abstraction #infinity #model checking #proving #reasoning #theorem proving #using

Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.

CAV-1995-GribomontR #named #verification

CAVEAT: Technique and Tool for Computer Aided VErification And Transformation (EPG, DR), pp. 70–83.

CAV-1995-RajanSS #automation #integration #model checking #proving

An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.

CAV-1995-HojatiB #abstraction #automation #hardware

Automatic Datapath Abstraction In Hardware Systems (RH, RKB), pp. 98–113.

CAV-1995-Rauzy #calculus #constraints #μ-calculus

Toupie = μ-Calculus + Constraints (AR), pp. 114–126.

CAV-1995-JagadeesanPO #safety #source code #verification

Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software (LJJ, CP, JVO), pp. 127–140.

CAV-1995-Emerson #calculus #model checking #tutorial #μ-calculus

Methods for μ-calculus Model Checking: A Tutorial (EAE), p. 141.

CAV-1995-AndersenV #behaviour #fixpoint #performance #using

Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion (HRA, BV), pp. 142–154.

CAV-1995-AzizSB #logic #probability

It Usually Works: The Temporal Logic of Stochastic Systems (AA, VS, FB), pp. 155–165.

CAV-1995-AlurH #composition #liveness #modelling

Local Liveness for Compositional Modeling of Fair Reactive Systems (RA, TAH), pp. 166–179.

CAV-1995-McMillan #using #verification

Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings (KLM), pp. 180–195.

CAV-1995-BouajjaniLR #automaton #calculus #hybrid #linear

From Duration Calculus To Linear Hybrid Automata (AB, YL, RR), pp. 196–210.

CAV-1995-SokolskyS #model checking #realtime

Local Model Checking for Real-Time Systems (OS, SAS), pp. 211–224.

CAV-1995-HenzingerH #algorithm #analysis #hybrid

Algorithmic Analysis of Nonlinear Hybrid Systems (TAH, PHH), pp. 225–238.

CAV-1995-Lescow #finite #game studies #on the #source code

On Polynomial-Size Programs Winning Finite-State Games (HL), pp. 239–252.

CAV-1995-KrishnanPBV #automaton #game studies

The Rabin Index and Chain Automata, with Applications to Automatas and Games (SCK, AP, RKB, PV), pp. 253–266.

CAV-1995-Vardi #approach #synthesis

An Automata-Theoretic Approach to Fair Realizability and Synthesis (MYV), pp. 267–278.

CAV-1995-AzizBBDS #finite #state machine

Supervisory Control of Finite State Machines (AA, FB, RKB, MDD, AS), pp. 279–292.

CAV-1995-CousotC #composition #constraints #equation #fixpoint #game studies #induction #rule-based #semantics

Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form (PC, RC), pp. 293–308.

CAV-1995-EmersonS #approach #model checking #symmetry

Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach (EAE, APS), pp. 309–324.

CAV-1995-Kupferman #branch #logic #quantifier

Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions (OK), pp. 325–338.

CAV-1995-KurshanMOS #modelling

Modelling Asynchrony with a Synchronous Model (RPK, MM, AO, SRS), pp. 339–352.

CAV-1995-EsparzaK #branch #logic #model checking #on the #parallel #problem #process

On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes (JE, AK), pp. 353–366.

CAV-1995-EirikssonM #analysis #case study #design #using #verification

Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study (ÁTE, KLM), pp. 367–380.

CAV-1995-HoW #analysis #automation #protocol

Automated Analysis of an Audio Control Protocol (PHH, HWT), pp. 381–394.

CAV-1995-FidgeKU #realtime #verification

Interactively Verifying a Simple Real-time Scheduler (CJF, PK, MU), pp. 395–408.

CAV-1995-DillW #approximate #realtime #verification

Verification of Real-Time Systems by Successive Over and Under Approximation (DLD, HWT), pp. 409–422.

CAV-1995-HulgaardB #analysis #performance #petri net

Efficient Timing Analysis of a Class of Petri Nets (HH, SMB), pp. 423–436.

CAV-1995-BouajjaniR #hybrid #linear #subclass #verification

Verifying ω-Regular Properties for a Subclass of Linear Hybrid Systems (AB, RR), pp. 437–450.