Aarti Gupta, Sharad Malik
Proceedings of the 20th International Conference on Computer Aided Verification
CAV, 2008.

@proceedings{CAV-2008,
	address       = "Princeton, New Jersey, USA",
	editor        = "Aarti Gupta and Sharad Malik",
	isbn          = "978-3-540-70543-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 20th International Conference on Computer Aided Verification}",
	volume        = 5123,
	year          = 2008,
}

Event page: http://www.princeton.edu/cav2008/

Contents (53 items)

11 ×#verification
8 ×#analysis
7 ×#named
5 ×#model checking
5 ×#proving
4 ×#abstraction
4 ×#approach
4 ×#concurrent
4 ×#memory management
4 ×#source code

CAV-2008-Larus #design #named

Singularity: Designing Better Software (JRL), pp. 1–2.

CAV-2008-Felten

Coping with Outside-the-Box Attacks (EWF), pp. 3–4.

CAV-2008-Foster #industrial #verification

Assertion-Based Verification: Industry Myths to Realities (HF), pp. 5–10.

CAV-2008-Harrison #proving #theorem proving #verification

Theorem Proving for Verification (JH), pp. 11–18.

CAV-2008-OHearn #logic #tutorial

Tutorial on Separation Logic (PWO), pp. 19–21.

CAV-2008-WilhelmW #abstract interpretation #validation

Abstract Interpretation with Applications to Timing Validation (RW, BW), pp. 22–36.

CAV-2008-LalR #analysis #bound #concurrent

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis (AL, TWR), pp. 37–51.

CAV-2008-FarzanM #concurrent #monitoring #source code

Monitoring Atomicity in Concurrent Programs (AF, PM), pp. 52–65.

CAV-2008-VakkalankaGK #order #reduction #source code #verification

Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings (SSV, GG, RMK), pp. 66–79.

CAV-2008-KobayashiS #hybrid #mobile #process #type system

A Hybrid Type System for Lock-Freedom of Mobile Processes (NK, DS), pp. 80–93.

CAV-2008-BaswanaMP #consistency #memory management #set #verification

Implied Set Closure and Its Application to Memory Consistency Verification (SB, SKM, VP), pp. 94–106.

CAV-2008-BurckhardtM #effectiveness #memory management #modelling #verification

Effective Program Verification for Relaxed Memory Models (SB, MM), pp. 107–120.

CAV-2008-CohenPZ #memory management #transaction #verification

Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses (AC, AP, LDZ), pp. 121–134.

CAV-2008-BobaruPG #abstraction #automation #reasoning #refinement

Automated Assume-Guarantee Reasoning by Abstraction Refinement (MGB, CSP, DG), pp. 135–148.

CAV-2008-CohenN #concurrent #linear #proving #source code

Local Proofs for Linear-Time Properties of Concurrent Programs (AC, KSN), pp. 149–161.

CAV-2008-HermannsWZ #probability

Probabilistic CEGAR (HH, BW, LZ), pp. 162–175.

CAV-2008-PlatzerC #difference #hybrid #invariant

Computing Differential Invariants of Hybrid Systems as Fixedpoints (AP, EMC), pp. 176–189.

CAV-2008-GulwaniT #analysis #approach #constraints #hybrid

Constraint-Based Approach for Analysis of Hybrid Systems (SG, AT), pp. 190–203.

CAV-2008-GadkariYSRMS #automation #embedded #generative #named

AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems (AAG, AY, JS, SR, SM, KCS), pp. 204–208.

CAV-2008-HolzerSTV #dynamic analysis #generative #metric #named #testing

FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement (AH, CS, MT, HV), pp. 209–213.

CAV-2008-JoshiK #graph transformation #theorem #verification

Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems (SJ, BK), pp. 214–226.

CAV-2008-DSouzaG

Conflict-Tolerant Features (DD, MG), pp. 227–239.

CAV-2008-AlurKW #automaton #game studies #ranking #requirements

Ranking Automata and Games for Prioritized Requirements (RA, AK, GW), pp. 240–253.

CAV-2008-JainCG #composition #equation #linear #performance

Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations (HJ, EMC, OG), pp. 254–267.

CAV-2008-PiskacK #linear

Linear Arithmetic with Stars (RP, VK), pp. 268–280.

CAV-2008-KingS #congruence #equation #satisfiability #using

Inferring Congruence Equations Using SAT (AK, HS), pp. 281–293.

CAV-2008-BofillNORR #smt

The Barcelogic SMT Solver (MB, RN, AO, ERC, AR), pp. 294–298.

CAV-2008-BruttomessoCFGS #smt

The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.

CAV-2008-BeyerZM #named

CSIsat: Interpolation for LA+EUF (DB, DZ, RM), pp. 304–308.

CAV-2008-MeikleF #approach #proving #verification

Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.

CAV-2008-PodelskiRW

Heap Assumptions on Demand (AP, AR, TW), pp. 314–327.

CAV-2008-CookGLRS #proving #termination

Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.

CAV-2008-AbdullaBCHR #abstraction #memory management #source code

Monotonic Abstraction for Programs with Dynamic Memory Heaps (PAA, AB, JC, FH, AR), pp. 341–354.

CAV-2008-NguyenC #verification

Enhancing Program Verification with Lemmas (HHN, WNC), pp. 355–369.

CAV-2008-GulavaniG #abstract domain #abstraction #analysis

A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis (BSG, SG), pp. 370–384.

CAV-2008-YangLBCCDO #analysis #scalability

Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.

CAV-2008-BerdineLMRS #analysis #concurrent #quantifier #thread

Thread Quantification for Concurrent Shape Analysis (JB, TLA, RM, GR, SS), pp. 399–413.

CAV-2008-Cremers #analysis #protocol #security #verification

The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols (CJFC), pp. 414–418.

CAV-2008-BackesLMP #abstraction #analysis #protocol #security

The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis (MB, SL, MM, KP), pp. 419–422.

CAV-2008-KinderV #framework #named #platform #static analysis

Jakstab: A Static Analysis Platform for Binaries (JK, HV), pp. 423–427.

CAV-2008-MagillTLT #named #reasoning

THOR: A Tool for Reasoning about Shape and Arithmetic (SM, MHT, PL, YKT), pp. 428–432.

CAV-2008-EisnerNY #composition #design #functional #power management #reasoning #verification

Functional Verification of Power Gated Designs by Compositional Reasoning (CE, AN, KY), pp. 433–445.

CAV-2008-Bjesse #approach #industrial #model checking #word

A Practical Approach to Word Level Model Checking of Industrial Netlists (PB), pp. 446–458.

CAV-2008-KunduLG #synthesis #validation

Validating High-Level Synthesis (SK, SL, RG), pp. 459–472.

CAV-2008-WienandWSKG #algebra #approach #correctness #proving

An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths (OW, MW, DS, WK, GMG), pp. 473–486.

CAV-2008-KimJRSPKS #analysis #random #simulation

Application of Formal Word-Level Analysis to Constrained Random Simulation (HK, HJ, KR, PS, JP, RPK, FS), pp. 487–490.

CAV-2008-KashyapG #using

Producing Short Counterexamples Using “Crucial Events” (SK, VKG), pp. 491–503.

CAV-2008-NiebertPP #model checking

Discriminative Model Checking (PN, DP, AP), pp. 504–516.

CAV-2008-GlabbeekP #algorithm #simulation

Correcting a Space-Efficient Simulation Algorithm (RJvG, BP), pp. 517–529.

CAV-2008-EdelkampSS #ltl #model checking

Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.

CAV-2008-GayNP #model checking #named #quantum

QMC: A Model Checker for Quantum Systems (SJG, RN, NP), pp. 543–547.

CAV-2008-Legay #model checking

T(O)RMC: A Tool for (ω)-Regular Model Checking (AL), pp. 548–551.

CAV-2008-KupferschmidWNP #performance #question

Faster Than Uppaal? (SK, MW, BN, AP), pp. 552–555.