BibSLEIGH — Proceedings of the 22nd International Conference on Computer Aided Verification

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

TEST

@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.

Tayssir Touili, Byron Cook, Paul JacksonProceedings of the 22nd International Conference on Computer Aided VerificationCAV, 2010.

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

Contents (58 items)

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