Proceedings of the 22nd 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

Tayssir Touili, Byron Cook, Paul Jackson
Proceedings of the 22nd International Conference on Computer Aided Verification
CAV, 2010.

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@proceedings{CAV-2010,
	address       = "Edinburgh, Scotland, United Kingdom",
	doi           = "10.1007/978-3-642-14295-6",
	editor        = "Tayssir Touili and Byron Cook and Paul Jackson",
	isbn          = "978-3-642-14294-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 22nd International Conference on Computer Aided Verification}",
	volume        = 6174,
	year          = 2010,
}

Event page: http://www.floc-conference.org/CAV-home.html

Contents (58 items)

CAV-2010-BasinKM #first-order #logic #monitoring #policy
Policy Monitoring in First-Order Temporal Logic (DAB, FK, SM), pp. 1–18.
CAV-2010-Jha #legacy #security
Retrofitting Legacy Code for Security (SJ), p. 19.
CAV-2010-Malacaria #data flow #question #theory and practice
Quantitative Information Flow: From Theory to Practice? (PM), pp. 20–22.
CAV-2010-Michael #algorithm #concurrent #memory management
Memory Management in Concurrent Algorithms (MMM), p. 23.
CAV-2010-BraytonM #named #verification
ABC: An Academic Industrial-Strength Verification Tool (RKB, AM), pp. 24–40.
CAV-2010-RepsLTBL #verification
There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.
CAV-2010-Rybalchenko #constraints #theorem proving #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CAV-2010-BouajjaniDERS #bound #invariant #source code #synthesis
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data (AB, CD, CE, AR, MS), pp. 72–88.
CAV-2010-KroeningSTW #analysis #composition #invariant #termination
Termination Analysis with Compositional Transition Invariants (DK, NS, AT, CMW), pp. 89–103.
CAV-2010-McMillan #lazy evaluation #testing #verification
Lazy Annotation for Program Testing and Verification (KLM), pp. 104–118.
CAV-2010-BallBLKL #framework #platform #research #verification
The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.
CAV-2010-KawaguchiRJ #named #safety #verification
Dsolve: Safety Verification via Liquid Types (MK, PMR, RJ), pp. 123–126.
CAV-2010-KunduGW #analysis #concurrent #named #testing
Contessa: Concurrency Testing Augmented with Symbolic Analysis (SK, MKG, CW), pp. 127–131.
CAV-2010-AbdullaCCHHMV #automaton #simulation #testing
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing (PAA, YFC, LC, LH, CDH, RM, TV), pp. 132–147.
CAV-2010-HerbreteauSW #automaton #performance
Efficient Emptiness Check for Timed Büchi Automata (FH, BS, IW), pp. 148–161.
CAV-2010-Caniart #model checking #named
Merit: An Interpolating Model-Checker (NC), pp. 162–166.
CAV-2010-Donze #hybrid #parametricity #synthesis #verification
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems (AD), pp. 167–170.
CAV-2010-PnueliSZ #algorithm #framework #named #verification
Jtlv: A Framework for Developing Verification Algorithms (AP, YS, LDZ), pp. 171–174.
CAV-2010-MeyerS #named #network
Petruchio: From Dynamic Networks to Nets (RM, TS), pp. 175–179.
CAV-2010-MariMST #feedback #hybrid #linear #synthesis
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems (FM, IM, IS, ET), pp. 180–195.
CAV-2010-ZhangSRHH #hybrid #probability #safety #verification
Safety Verification for Probabilistic Hybrid Systems (LZ, ZS, SR, HH, EMH), pp. 196–211.
CAV-2010-GhorbalGP #approach #logic
A Logical Product Approach to Zonotope Intersection (KG, EG, SP), pp. 212–226.
CAV-2010-BozgaIK #performance
Fast Acceleration of Ultimately Periodic Relations (MB, RI, FK), pp. 227–242.
CAV-2010-PulinaT #abstraction #approach #network #verification
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (LP, AT), pp. 243–257.
CAV-2010-AlglaveMSS #memory management #modelling
Fences in Weak Memory Models (JA, LM, SS, PS), pp. 258–272.
CAV-2010-Mador-HaimAM #consistency #generative #memory management #modelling #testing
Generating Litmus Tests for Contrasting Memory Consistency Models (SMH, RA, MMKM), pp. 273–287.
CAV-2010-ThakurLLBDEAR #generative #proving
Directed Proof Generation for Machine Code (AVT, JL, AL, AB, ED, ME, TA, TWR), pp. 288–305.
CAV-2010-ConwayB #data type #implementation #low level #verification
Verifying Low-Level Implementations of High-Level Datatypes (CLC, CB), pp. 306–320.
CAV-2010-ChatterjeeK #architecture #automation #communication #generative #induction #invariant #modelling
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics (SC, MK), pp. 321–338.
CAV-2010-LiXBL #analysis #automaton #hardware #performance #reachability
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification (JL, FX, TB, VL), pp. 339–353.
CAV-2010-BlomPW #distributed #named #reachability
LTSmin: Distributed and Symbolic Reachability (SB, JvdP, MW), pp. 354–359.
CAV-2010-BolligKKLNP #automaton #framework #learning #named
libalf: The Automata Learning Framework (BB, JPK, CK, ML, DN, DRP), pp. 360–364.
CAV-2010-Ehlers #bound #synthesis
Symbolic Bounded Synthesis (RE), pp. 365–379.
CAV-2010-ChatterjeeHJS #probability
Measuring and Synthesizing Systems in Probabilistic Environments (KC, TAH, BJ, RS), pp. 380–395.
CAV-2010-GrafPQ #distributed #model checking
Achieving Distributed Control through Model Checking (SG, DP, SQ), pp. 396–409.
CAV-2010-BloemCGHJ #liveness #robust
Robustness in the Presence of Liveness (RB, KC, KG, TAH, BJ), pp. 410–424.
CAV-2010-BloemCGHKRSS #analysis #named #requirements #synthesis
RATSY — A New Requirements Analysis Tool with Synthesis (RB, AC, KG, GH, RK, MR, VS, RS), pp. 425–429.
CAV-2010-KuncakMPS #functional #named #synthesis
Comfusy: A Tool for Complete Functional Synthesis (VK, MM, RP, PS), pp. 430–433.
CAV-2010-KahlonW #concurrent #debugging #detection #graph #precise #source code
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs (VK, CW), pp. 434–449.
CAV-2010-Vafeiadis #automation #proving
Automatically Proving Linearizability (VV), pp. 450–464.
CAV-2010-CernyRZCA #concurrent #implementation #model checking
Model Checking of Linearizability of Concurrent List Implementations (PC, AR, DZ, SC, RA), pp. 465–479.
CAV-2010-CohenMST #concurrent #invariant #source code #verification
Local Verification of Global Invariants in Concurrent Programs (EC, MM, WS, ST), pp. 480–494.
CAV-2010-AlbarghouthiGWC #analysis #symbolic computation
Abstract Analysis of Symbolic Executions (AA, AG, OW, MC), pp. 495–510.
CAV-2010-ChenCFTTW #automation #learning #reasoning
Automated Assume-Guarantee Reasoning through Implicit Learning (YFC, EMC, AF, MHT, YKT, BYW), pp. 511–526.
CAV-2010-SinghGP #abstraction #component #interface #learning
Learning Component Interfaces with May and Must Abstractions (RS, DG, CSP), pp. 527–542.
CAV-2010-CohenNS #composition #reasoning
A Dash of Fairness for Compositional Reasoning (AC, KSN, YS), pp. 543–557.
CAV-2010-CohenNS10a #composition #ltl #named #verification
SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.
CAV-2010-BozzanoCKNNRW #model checking
A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
CAV-2010-MazoDT #embedded #named #synthesis
PESSOA: A Tool for Embedded Controller Synthesis (MMJ, AD, PT), pp. 566–569.
CAV-2010-ZhouHWG #array #bound #on the
On Array Theory of Bounded Elements (MZ, FH, BYW, MG), pp. 570–584.
CAV-2010-Monniaux #lazy evaluation #quantifier
Quantifier Elimination by Lazy Model Enumeration (DM), pp. 585–599.
CAV-2010-GantyMM #approximate #bound
Bounded Underapproximations (PG, RM, BM), pp. 600–614.
CAV-2010-Seth #automaton #bound #multi #reachability
Global Reachability in Bounded Phase Multi-stack Pushdown Systems (AS), pp. 615–628.
CAV-2010-TorreMP #concurrent #interface #linear #model checking #source code #using
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces (SLT, PM, GP), pp. 629–644.
CAV-2010-KaiserKW #concurrent #detection #source code
Dynamic Cutoff Detection in Parameterized Concurrent Programs (AK, DK, TW), pp. 645–659.
CAV-2010-HahnHWZ #markov #model checking #modelling #named #parametricity
PARAM: A Model Checker for Parametric Markov Models (EMH, HH, BW, LZ), pp. 660–664.
CAV-2010-ChatterjeeHJR #game studies #named #probability
Gist: A Solver for Probabilistic Games (KC, TAH, BJ, AR), pp. 665–669.
CAV-2010-FerranteMNPS #model checking
A NuSMV Extension for Graded-CTL Model Checking (AF, MM, MN, MP, FS), pp. 670–673.

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.