Warren A. Hunt Jr., Fabio Somenzi
Proceedings of the 15th International Conference on Computer Aided Verification
CAV, 2003.

@proceedings{CAV-2003,
	address       = "Boulder, Colorado, USA",
	editor        = "Warren A. Hunt Jr. and Fabio Somenzi",
	isbn          = "3-540-40524-0",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 15th International Conference on Computer Aided Verification}",
	volume        = 2725,
	year          = 2003,
}

Contents (41 items)

10 ×#model checking
6 ×#abstraction
5 ×#logic
5 ×#named
5 ×#verification
4 ×#performance
4 ×#using
3 ×#automaton
3 ×#bound
2 ×#algorithm

CAV-2003-McMillan #model checking #satisfiability

Interpolation and SAT-Based Model Checking (KLM), pp. 1–13.

CAV-2003-MouraRS #bound #induction #model checking #verification

Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) (LMdM, HR, MS), pp. 14–26.

CAV-2003-EisnerFHLMC #logic #reasoning

Reasoning with Temporal Logic on Truncated Paths (CE, DF, JH, YL, AM, DVC), pp. 27–39.

CAV-2003-CiardoS #model checking

Structural Symbolic CTL Model Checking of Asynchronous Systems (GC, RS), pp. 40–53.

CAV-2003-GrumbergHS #algorithm #analysis #distributed #reachability

A Work-Efficient Distributed Algorithm for Reachability Analysis (OG, TH, AS), pp. 54–66.

CAV-2003-AlurTM #composition #game studies #graph #infinity #recursion

Modular Strategies for Infinite Games on Recursive Graphs (RA, SLT, PM), pp. 67–79.

CAV-2003-Obdrzalek #bound #calculus #model checking #performance #μ-calculus

Fast μ-Calculus Model Checking when Tree-Width Is Bounded (JO), pp. 80–92.

CAV-2003-XieDIP #problem #verification

Dense Counter Machines and Verification Problems (GX, ZD, OHI, PSP), pp. 93–105.

CAV-2003-SenguptaC #named #sequence chart

TRIM: A Tool for Triggered Message Sequence Charts (BS, RC), pp. 106–109.

CAV-2003-BordiniFPVW #model checking #multi #source code

Model Checking Multi-Agent Programs with CASP (RHB, MF, CP, WV, MW), pp. 110–113.

CAV-2003-Drusinsky #monitoring

Monitoring Temporal Rules Combined with Time Series (DD), pp. 114–117.

CAV-2003-BardinFLP #named #performance

FAST: Fast Acceleration of Symbolikc Transition Systems (SB, AF, JL, LP), pp. 118–121.

CAV-2003-BeyerLN #named #realtime #verification

Rabbit: A Tool for BDD-Based Verification of Real-Time Systems (DB, CL, AN), pp. 122–125.

CAV-2003-ClarkeGTW #abstraction #how #performance

Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates (EMC, OG, MT, DW), pp. 126–140.

CAV-2003-LahiriBC #abstraction #approach

A Symbolic Approach to Predicate Abstraction (SKL, REB, BC), pp. 141–153.

CAV-2003-SeshiaB #automaton #bound #model checking #using

Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods (SAS, REB), pp. 154–166.

CAV-2003-ChakravortyP #logic

Digitizing Interval Duration Logic (GC, PKP), pp. 167–179.

CAV-2003-BouyerDMP

Timed Control with Partial Observability (PB, DD, PM, AP), pp. 180–192.

CAV-2003-BoigelotHJ #automaton #hybrid #using

Hybrid Acceleration Using Real Vector Automata (BB, FH, SJ), pp. 193–205.

CAV-2003-GuptaGWYA #abstraction #satisfiability

Abstraction and BDDs Complement SAT-Based BMC in DiVer (AG, MKG, CW, ZY, PA), pp. 206–209.

CAV-2003-ChechikG #logic #named #query

TLQSolver: A Temporal Logic Query Checker (MC, AG), pp. 210–214.

CAV-2003-DongRS #model checking #proving

Evidence Explorer: A Tool for Exploring Model-Checking Proofs (YD, CRR, SAS), pp. 215–218.

CAV-2003-BozgaLP #automation #named #protocol #security #verification

HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols (LB, YL, MP), pp. 219–222.

CAV-2003-BoigelotLW #in the large #transducer

Iterating Transducers in the Large (BB, AL, PW), pp. 223–235.

CAV-2003-AbdullaJNd #algorithm #model checking

Algorithmic Improvements in Regular Model Checking (PAA, BJ, MN, Jd), pp. 236–248.

CAV-2003-BartzisB #image #infinity #model checking #performance

Efficient Image Computation in Infinite State Model Checking (CB, TB), pp. 249–261.

CAV-2003-HenzingerJMQ #abstraction #refinement #thread

Thread-Modular Abstraction Refinement (TAH, RJ, RM, SQ), pp. 262–274.

CAV-2003-ShohamG #abstraction #framework #game studies

A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement (SS, OG), pp. 275–287.

CAV-2003-Namjoshi #abstraction #branch

Abstraction for Branching Time Properties (KSN), pp. 288–300.

CAV-2003-RosuVWL #estimation #source code

Certifying Optimality of State Estimation Programs (GR, RPV, JW, LL), pp. 301–314.

CAV-2003-HungarNS #automaton #learning #optimisation

Domain-Specific Optimization in Automata Learning (HH, ON, BS), pp. 315–327.

CAV-2003-GlusmanK #consistency #model checking #specification

Model Checking Conformance with Scenario-Based Specifications (MG, SK), pp. 328–340.

CAV-2003-LahiriB #deduction #verification

Deductive Verification of Advanced Out-of-Order Microprocessors (SKL, REB), pp. 341–353.

CAV-2003-FlanaganJOS #lazy evaluation #proving #theorem proving #using

Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.

CAV-2003-ArmoniFFGPTV #detection #linear #logic

Enhanced Vacuity Detection in Linear Temporal Logic (RA, LF, AF, OG, NP, AT, MYV), pp. 368–380.

CAV-2003-KestenPP #simulation

Bridging the Gap between Fair Simulation and Trace Inclusion (YK, NP, AP), pp. 381–393.

CAV-2003-Geilen #logic #on the fly #realtime

An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic (MG), pp. 394–406.

CAV-2003-Abu-HaimedBD #consistency #invariant #testing

Strengthening Invariants by Symbolic Consistency Testing (HAH, SB, DLD), pp. 407–419.

CAV-2003-ColonSS #constraints #generative #invariant #linear #theorem proving #using

Linear Invariant Generation Using Non-linear Constraint Solving (MC, SS, HS), pp. 420–432.

CAV-2003-BehrmannLP

To Store or Not to Store (GB, KGL, RP), pp. 433–445.

CAV-2003-PaceLM

Calculating-Confluence Compositionally (GJP, FL, RM), pp. 446–459.