BibSLEIGH — Proceedings of the 26th International Conference on Computer Aided Verification

Armin Biere, Roderick Bloem
Proceedings of the 26th International Conference on Computer Aided Verification
CAV, 2014.

TEST

@proceedings{CAV-2014,
	address       = "Vienna, Austria",
	doi           = "10.1007/978-3-319-08867-9",
	editor        = "Armin Biere and Roderick Bloem",
	isbn          = "978-3-319-08866-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 26th International Conference on Computer Aided Verification}",
	volume        = 8559,
	year          = 2014,
}

Event page: http://i-cav.org/2014/

Contents (57 items)

CAV-2014-FilliatreGP: The Spirit of Ghost Code (JCF, LG, AP), pp. 1–16.
CAV-2014-KomuravelliGC #model checking #recursion #smt #source code: SMT-Based Model Checking for Recursive Programs (AK, AG, SC), pp. 17–34.
CAV-2014-ItzhakyBRST #analysis: Property-Directed Shape Analysis (SI, NB, TWR, MS, AVT), pp. 35–51.
CAV-2014-LeGQC #analysis #higher-order: Shape Analysis via Second-Order Bi-Abduction (QLL, CG, SQ, WNC), pp. 52–68.
CAV-2014-0001LMN #framework #invariant #learning #named #robust: ICE: A Robust Framework for Learning Invariants (PG, CL, PM, DN), pp. 69–87.
CAV-2014-0001A #invariant #random #using: From Invariant Checking to Invariant Inference Using Randomized Search (RS, AA), pp. 88–105.
CAV-2014-RakamaricE #implementation #named #verification: SMACK: Decoupling Source Language Details from Verifier Implementations (ZR, ME), pp. 106–113.
CAV-2014-EldibW #synthesis: Synthesis of Masking Countermeasures against Side Channel Attacks (HE, CW), pp. 114–130.
CAV-2014-ChowdhuryJGD #monitoring #policy #privacy #runtime: Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (OC, LJ, DG, AD), pp. 131–149.
CAV-2014-AbdullaACHRRS #constraints #string #verification: String Constraints for Verification (PAA, MFA, YFC, LH, AR, PR, JS), pp. 150–166.
CAV-2014-KanavL0 #documentation: A Conference Management System with Verified Document Confidentiality (SK, PL, AP), pp. 167–183.
CAV-2014-FerraraMNP #data access #named #policy #verification: Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.
CAV-2014-EsparzaK #approach #automaton #composition #ltl: From LTL to Deterministic Automata: A Safraless Compositional Approach (JE, JK), pp. 192–208.
CAV-2014-DAntoniA #automaton: Symbolic Visibly Pushdown Automata (LD, RA), pp. 209–225.
CAV-2014-BardsleyBCCDDKLQ #gpu #kernel #verification: Engineering a Static Verification Tool for GPU Kernels (EB, AB, NC, PC, PD, AFD, JK, DL, SQ), pp. 226–242.
CAV-2014-McMillan #lazy evaluation #revisited: Lazy Annotation Revisited (KLM), pp. 243–259.
CAV-2014-VizelG #reachability: Interpolating Property Directed Reachability (YV, AG), pp. 260–276.
CAV-2014-BinghamL #bound #fault #simulation #using #verification: Verifying Relative Error Bounds Using Symbolic Simulation (JB, JLH), pp. 277–292.
CAV-2014-GligoricMSEM #distributed #testing: Regression Test Selection for Distributed Software Histories (MG, RM, RS, LE, DM), pp. 293–309.
CAV-2014-WijsKB #component #composition #graph: GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (AW, JPK, DB), pp. 310–326.
CAV-2014-BeyerDW #verification: Software Verification in the Google App-Engine Cloud (DB, GD, PW), pp. 327–333.
CAV-2014-CavadaCDGMMMRT #model checking: The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
CAV-2014-PaolettiYHWK #logic: Analyzing and Synthesizing Genomic Logic Functions (NP, BY, YH, CMW, HK), pp. 343–357.
CAV-2014-CookFHIJP #biology #modelling: Finding Instability in Biological Models (BC, JF, BAH, SI, GJ, NP), pp. 358–372.
CAV-2014-HuangFMMK #automaton #hybrid #invariant #network #verification: Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells (ZH, CF, AM, SM, MZK), pp. 373–390.
CAV-2014-HansenLLN0 #abstraction #automaton #partial order #reduction #women: Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions (HH, SWL, YL, TKN, JS), pp. 391–406.
CAV-2014-Hagemann #analysis #hybrid #orthogonal #reachability #using: Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (WH), pp. 407–423.
CAV-2014-CimattiGMT #hybrid #ltl #verification: Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
CAV-2014-BozianuDF #specification #synthesis: Safraless Synthesis for Epistemic Temporal Specifications (RB, CD, EF), pp. 441–456.
CAV-2014-BrazdilKKN #low cost: Minimizing Running Costs in Consumption Systems (TB, DK, AK, PN), pp. 457–472.
CAV-2014-ChatterjeeCD #analysis #probability: CEGAR for Qualitative Analysis of Probabilistic Systems (KC, MC, PD), pp. 473–490.
CAV-2014-DilligDC #memory management #safety #synthesis: Optimal Guard Synthesis for Memory Safety (TD, ID, SC), pp. 491–507.
CAV-2014-AlglaveKNP #approach #automation #static analysis: Don’t Sit on the Fence — A Static Analysis Approach to Automatic Fence Insertion (JA, DK, VN, DP), pp. 508–524.
CAV-2014-CermakLMM #logic #model checking #named #specification #verification: MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (PC, AL, FM, AM), pp. 525–532.
CAV-2014-NarodytskaLBRW #game studies: Solving Games without Controllable Predecessor (NN, AL, FB, LR, AW), pp. 533–540.
CAV-2014-ChengHRS #automation #generative #named #source code: G4LTL-ST: Automatic Generation of PLC Programs (CHC, CHH, HR, SS), pp. 541–549.
CAV-2014-LesaniMP #automation #concurrent #data type #verification: Automatic Atomicity Verification for Clients of Concurrent Data Structures (ML, TDM, JP), pp. 550–567.
CAV-2014-CernyHRRT #concurrent #synthesis: Regression-Free Synthesis for Concurrency (PC, TAH, AR, LR, TT), pp. 568–584.
CAV-2014-InversoT0TP #bound #c #concurrent #lazy evaluation #model checking #multi #source code #thread: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization (OI, ET, BF, SLT, GP), pp. 585–602.
CAV-2014-EsparzaLMMN #analysis #approach #smt: An SMT-Based Approach to Coverability Analysis (JE, RLG, RM, PM, FN), pp. 603–619.
CAV-2014-SanchezS #concurrent #data type #named #verification: LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (AS, CS), pp. 620–627.
CAV-2014-VeanesBNB #composition #monad: Monadic Decomposition (MV, NB, LN, SB), pp. 628–645.
CAV-2014-LiangRTBD #formal method #regular expression #string: A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (TL, AR, CT, CB, MD), pp. 646–662.
CAV-2014-Nadel #automation #generative: Bit-Vector Rewriting with Automatic Rule Generation (AN), pp. 663–679.
CAV-2014-HadareanBJBT #lazy evaluation: A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors (LH, KB, DJ, CB, CT), pp. 680–695.
CAV-2014-Voronkov #architecture #first-order #named #proving #theorem proving: AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
CAV-2014-PiskacWZ #automation #logic: Automating Separation Logic with Trees and Data (RP, TW, DZ), pp. 711–728.
CAV-2014-TiwariL: A Nonlinear Real Arithmetic Fragment (AT, PL), pp. 729–736.
CAV-2014-Dutertre: Yices 2.2 (BD), pp. 737–744.
CAV-2014-SinnZV #bound #complexity #scalability #static analysis: A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (MS, FZ, HV), pp. 745–761.
CAV-2014-MadhavanK #bound #functional #source code: Symbolic Resource Bound Inference for Functional Programs (RM, VK), pp. 762–778.
CAV-2014-LarrazNORR #proving #using: Proving Non-termination Using Max-SMT (DL, KN, AO, ERC, AR), pp. 779–796.
CAV-2014-HeizmannHP #analysis #learning #source code #termination: Termination Analysis by Learning Terminating Programs (MH, JH, AP), pp. 797–813.
CAV-2014-KupriyanovF #concurrent #multi #source code #termination #thread: Causal Termination of Multi-threaded Programs (AK, BF), pp. 814–830.
CAV-2014-BirgmeierBW #abstraction #induction: Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (JB, ARB, GW), pp. 831–848.
CAV-2014-LeeS #abstraction #approximate #bound #reachability #scalability #verification: Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (SL, KAS), pp. 849–865.
CAV-2014-CoxCS #abstraction #library #named #parametricity #reuse #set: QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (AC, BYEC, SS), pp. 866–873.

Armin Biere, Roderick BloemProceedings of the 26th International Conference on Computer Aided VerificationCAV, 2014.

Event page: http://i-cav.org/2014/

Contents (57 items)

Armin Biere, Roderick Bloem
Proceedings of the 26th International Conference on Computer Aided Verification
CAV, 2014.