Proceedings of the 20th International Conference on Computer Aided Verification
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.