Kousha Etessami, Sriram K. Rajamani
Proceedings of the 17th International Conference on Computer Aided Verification
CAV, 2005.

@proceedings{CAV-2005,
	address       = "Edinburgh, Scotland, United Kingdom",
	editor        = "Kousha Etessami and Sriram K. Rajamani",
	isbn          = "3-540-27231-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 17th International Conference on Computer Aided Verification}",
	volume        = 3576,
	year          = 2005,
}

Event page: http://www.cav2005.inf.ed.ac.uk/

Contents (52 items)

13 ×#verification
11 ×#model checking
11 ×#named
4 ×#abstraction
4 ×#algorithm
4 ×#satisfiability
3 ×#bound
3 ×#concurrent
3 ×#framework
3 ×#performance

CAV-2005-NeculaG #algorithm #program analysis #random #verification

Randomized Algorithms for Program Analysis and Verification (GCN, SG), p. 1.

CAV-2005-Bentley #validation

Validating a Modern Microprocessor (BB), pp. 2–4.

CAV-2005-PiazzaAMPWM #algebra #algorithm #biology #challenge #model checking

Algorithmic Algebraic Model Checking I: Challenges from Systems Biology (CP, MA, VM, AP, FW, BM), pp. 5–19.

CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability

SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.

CAV-2005-LahiriBC #abstraction

Predicate Abstraction via Symbolic Decision Procedures (SKL, TB, BC), pp. 24–38.

CAV-2005-JhalaM #approximate

Interpolant-Based Transition Relation Approximation (RJ, KLM), pp. 39–51.

CAV-2005-PasareanuPV #model checking #refinement

Concrete Model Checking with Abstract Matching and Refinement (CSP, RP, WV), pp. 52–66.

CAV-2005-BallKY #abstraction

Abstraction for Falsification (TB, OK, GY), pp. 67–81.

CAV-2005-RabinovitzG #bound #concurrent #model checking #source code

Bounded Model Checking of Concurrent Programs (IR, OG), pp. 82–97.

CAV-2005-HeljankoJL #bound #incremental #model checking

Incremental and Complete Bounded Model Checking for Full PLTL (KH, TAJ, TL), pp. 98–111.

CAV-2005-GuptaS #abstraction #bound #model checking #refinement

Abstraction Refinement for Bounded Model Checking (AG, OS), pp. 112–124.

CAV-2005-TangMGI #model checking #reduction #satisfiability #symmetry

Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.

CAV-2005-XieA #debugging #detection #named #satisfiability

Saturn: A SAT-Based Tool for Bug Detection (YX, AA), pp. 139–143.

CAV-2005-ChanderEILN #java #named #verification

JVer: A Java Verifier (AC, DE, NI, PL, GCN), pp. 144–147.

CAV-2005-DwyerHHR #framework #model checking #using

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.

CAV-2005-BarnerGR #concurrent #debugging #formal method #named #using

Wolf — Bug Hunter for Concurrent Software Using Formal Methods (SB, ZG, IR), pp. 153–157.

CAV-2005-BalakrishnanRKLLMGYCT #bytecode #model checking

Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ (GB, TWR, NK, AL, JL, DM, RG, SHY, CHC, TT), pp. 158–163.

CAV-2005-ChakiISW #framework #reasoning

The ComFoRT Reasoning Framework (SC, JI, NS, KCW), pp. 164–169.

CAV-2005-Kaivola #component #induction #invariant #simulation #verification

Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants (RK), pp. 170–184.

CAV-2005-AronsEFMMSSTVZ #verification

Formal Verification of Backward Compatibility of Microcode (TA, EE, LF, SMH, MM, JS, ES, AT, MYV, LDZ), pp. 185–198.

CAV-2005-Monniaux #analysis #composition #float #linear

Compositional Analysis of Floating-Point Linear Numerical Filters (DM), pp. 199–212.

CAV-2005-VecchieS #source code

Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs (EV, RdS), pp. 213–225.

CAV-2005-JobstmannGB #game studies #program repair

Program Repair as a Game (BJ, AG, RB), pp. 226–238.

CAV-2005-0002G #modelling #probability #protocol #verification

Improved Probabilistic Models for 802.11 Protocol Verification (AR, KG), pp. 239–252.

CAV-2005-Younes #black box #probability #verification

Probabilistic Verification for “Black-Box” Systems (HLSY), pp. 253–265.

CAV-2005-SenVA #model checking #on the #probability #statistics

On Statistical Model Checking of Stochastic Systems (KS, MV, GA), pp. 266–280.

CAV-2005-ArmandoBBCCCDHKMMORSTVV #automation #internet #protocol #security #validation

The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications (AA, DAB, YB, YC, LC, JC, PHD, PCH, OK, JM, SM, DvO, MR, JS, MT, LV, LV), pp. 281–285.

CAV-2005-OlivainG #detection

The Orchids Intrusion Detection Tool (JO, JGL), pp. 286–290.

CAV-2005-BarrettFGHPZ #compilation #named #optimisation #validation

TVOC: A Translation Validator for Optimizing Compilers (CWB, YF, BG, YH, AP, LDZ), pp. 291–295.

CAV-2005-CookKS #named #proving #theorem proving #verification

Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.

CAV-2005-IvancicYGGSA #framework #named #platform #verification

F-Soft: Software Verification Platform (FI, ZY, MKG, AG, IS, PA), pp. 301–306.

CAV-2005-MeirS #logic #similarity

Yet Another Decision Procedure for Equality Logic (OM, OS), pp. 307–320.

CAV-2005-NieuwenhuisO #difference #logic

DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic (RN, AO), pp. 321–334.

CAV-2005-BozzanoBCJRRS #modulo theories #performance #satisfiability

Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.

CAV-2005-SebastianiTV #hybrid #ltl #model checking

Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.

CAV-2005-dAmorimR #monitoring #performance

Efficient Monitoring of ω-Languages (Md, GR), pp. 364–378.

CAV-2005-BenediktBFV #optimisation #verification

Verification of Tree Updates for Optimization (MB, AB, SF, AV), pp. 379–393.

CAV-2005-GeeraertsRB #performance

Expand, Enlarge and Check... Made Efficient (GG, JFR, LVB), pp. 394–407.

CAV-2005-BalabanFPZ #invariant #named #verification

IIV: An Invisible Invariant Verifier (IB, YF, AP, LDZ), pp. 408–412.

CAV-2005-Yavuz-KahveciBB #verification

Action Language Verifier, Extended (TYK, CB, TB), pp. 413–417.

CAV-2005-GardeyLMR #named #petri net

Romeo: A Tool for Analyzing Time Petri Nets (GG, DL, MM, OHR), pp. 418–423.

CAV-2005-PastorPS #concurrent #named #verification

TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems (EP, MAP, MS), pp. 424–428.

CAV-2005-Younes05a #model checking #named #statistics

Ymer: A Statistical Model Checker (HLSY), pp. 429–433.

CAV-2005-LalRB #automaton

Extended Weighted Pushdown Systems (AL, TWR, GB), pp. 434–448.

CAV-2005-ConwayNDE #algorithm #analysis #incremental #interprocedural #safety

Incremental Algorithms for Inter-procedural Analysis of Safety Properties (CLC, KSN, DD, SAE), pp. 449–461.

CAV-2005-CostanGGMP #algorithm #fixpoint #policy #source code #static analysis

A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs (AC, SG, EG, MM, SP), pp. 462–475.

CAV-2005-McPeakN #axiom #data type #similarity #specification

Data Structure Specifications via Local Equality Axioms (SM, GCN), pp. 476–490.

CAV-2005-BradleyMS #linear #ranking #reachability

Linear Ranking with Reachability (ARB, ZM, HBS), pp. 491–504.

CAV-2005-KahlonIG #communication #reasoning #thread

Reasoning About Threads Communicating via Locks (VK, FI, AG), pp. 505–518.

CAV-2005-LoginovRS #abstraction #induction #learning #refinement

Abstraction Refinement via Inductive Learning (AL, TWR, SS), pp. 519–533.

CAV-2005-ChakiCST #automation #consistency #reasoning #simulation

Automated Assume-Guarantee Reasoning for Simulation Conformance (SC, EMC, NS, PT), pp. 534–547.

CAV-2005-AlurMN #composition #learning #verification

Symbolic Compositional Verification by Learning Assumptions (RA, PM, WN), pp. 548–562.