BibSLEIGH — Proceedings of the 23rd International Conference on Computer Aided Verification

Ganesh Gopalakrishnan, Shaz Qadeer
Proceedings of the 23rd International Conference on Computer Aided Verification
CAV, 2011.

TEST

@proceedings{CAV-2011,
	address       = "Snowbird, Utah, USA",
	doi           = "10.1007/978-3-642-22110-1",
	editor        = "Ganesh Gopalakrishnan and Shaz Qadeer",
	isbn          = "978-3-642-22109-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 23rd International Conference on Computer Aided Verification}",
	volume        = 6806,
	year          = 2011,
}

Contents (60 items)

CAV-2011-GaneshKAGHE #analysis #detection #named #string #testing: HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection (VG, AK, SA, PJG, PH, MDE), pp. 1–19.
CAV-2011-Jhala #using #verification: Using Types for Software Verification (RJ), p. 20.
CAV-2011-Lahiri #analysis #composition #smt: SMT-Based Modular Analysis of Sequential Systems Code (SKL), pp. 21–27.
CAV-2011-Platzer #composition #hybrid #logic #verification: Logic and Compositional Verification of Hybrid Systems — (AP), pp. 28–43.
CAV-2011-SinghalA #simulation #using #verification: Using Coverage to Deploy Formal Verification in a Simulation World (VS, PA), pp. 44–49.
CAV-2011-AlglaveM #memory management #modelling: Stability in Weak Memory Models (JA, LM), pp. 50–66.
CAV-2011-AlkassarBMR #verification: Verification of Certifying Computations (EA, SB, KM, CR), pp. 67–82.
CAV-2011-AndreychenkoMSW #identification #markov #modelling #parametricity: Parameter Identification for Markov Models of Biochemical Reactions (AA, LM, DS, VW), pp. 83–98.
CAV-2011-AtigBP #analysis: Getting Rid of Store-Buffers in TSO Analysis (MFA, AB, GP), pp. 99–115.
CAV-2011-BabicRS #analysis #automaton: Malware Analysis with Tree Automata Inference (DB, DR, DS), pp. 116–131.
CAV-2011-BaeM #ltl #model checking #parametricity: State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
CAV-2011-BalabanovJ #evaluation #proving: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications (VB, JHRJ), pp. 149–164.
CAV-2011-BardinHLLTV #analysis #framework: The BINCOA Framework for Binary Code Analysis (SB, PH, JL, OL, RT, AV), pp. 165–170.
CAV-2011-BarrettCDHJKRT: CVC4 (CB, CLC, MD, LH, DJ, TK, AR, CT), pp. 171–177.
CAV-2011-BerdineCI #memory management #named #safety: SLAyer: Memory Safety for Systems-Level Code (JB, BC, SI), pp. 178–183.
CAV-2011-BeyerK #configuration management #named #verification: CPAchecker: A Tool for Configurable Software Verification (DB, MEK), pp. 184–190.
CAV-2011-BrauerKK #incremental #quantifier #satisfiability: Existential Quantification as Incremental SAT (JB, AK, JK), pp. 191–207.
CAV-2011-BrazdilKK #analysis #bound #performance #probability #source code: Efficient Analysis of Probabilistic Programs with an Unbounded Counter (TB, SK, AK), pp. 208–224.
CAV-2011-BuchholzHHZ #algorithm #model checking: Model Checking Algorithms for CTMDPs (PB, EMH, HH, LZ), pp. 225–242.
CAV-2011-CernyCHRS #concurrent #source code #synthesis: Quantitative Synthesis for Concurrent Programs (PC, KC, TAH, AR, RS), pp. 243–259.
CAV-2011-ChatterjeeHJS #algorithm #analysis #automaton #markov #process: Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives (KC, MH, MJ, NS), pp. 260–276.
CAV-2011-ChaudhuriS #robust: Smoothing a Program Soundly and Robustly (SC, ASL), pp. 277–292.
CAV-2011-ChinGVLCQ #calculus #verification: A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification (WNC, CG, RV, QLL, FC, SQ), pp. 293–309.
CAV-2011-CimattiGMNR #model checking #named: Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
CAV-2011-CimattiMT #automaton #hybrid #performance #verification: Efficient Scenario Verification for Hybrid Automata (AC, SM, ST), pp. 317–332.
CAV-2011-CookKV #program analysis #verification: Temporal Property Verification as a Program Analysis Task (BC, EK, MYV), pp. 333–348.
CAV-2011-DavidLLMW #model checking #realtime #statistics: Time for Statistical Model Checking of Real-Time Systems (AD, KGL, AL, MM, ZW), pp. 349–355.
CAV-2011-DonaldsonKKW #abstraction #concurrent #source code #symmetry: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (AFD, AK, DK, TW), pp. 356–371.
CAV-2011-DudkaPV #data type #logic #named #using: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic (KD, PP, TV), pp. 372–378.
CAV-2011-FrehseGDCRLRGDM #hybrid #named #scalability #verification: SpaceEx: Scalable Verification of Hybrid Systems (GF, CLG, AD, SC, RR, OL, RR, AG, TD, OM), pp. 379–395.
CAV-2011-GrosuBFGGSB #network #search-based: From Cardiac Cells to Genetic Regulatory Networks (RG, GB, FHF, JG, CLG, SAS, EB), pp. 396–411.
CAV-2011-GuptaPR #concurrent #constraints #multi #named #source code #thread #verification: Threader: A Constraint-Based Verifier for Multi-threaded Programs (AG, CP, AR), pp. 412–417.
CAV-2011-GveroKP #interactive #synthesis: Interactive Synthesis of Code Snippets (TG, VK, RP), pp. 418–423.
CAV-2011-HabermehlHRSV #automaton #verification: Forest Automata for Verification of Heap Manipulation (PH, LH, AR, JS, TV), pp. 424–440.
CAV-2011-HangMP #architecture #constraints #cyber-physical #modelling #realtime: Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints (CH, PM, VP), pp. 441–456.
CAV-2011-HoderBM #constraints #fixpoint #named #performance: μZ — An Efficient Engine for Fixed Points with Constraints (KH, NB, LMdM), pp. 457–462.
CAV-2011-BrumleyJAS #analysis #framework #named #platform: BAP: A Binary Analysis Platform (DB, IJ, TA, EJS), pp. 463–469.
CAV-2011-JhalaMR #functional #named #source code #using #verification: HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.
CAV-2011-JohnC #algorithm #composition #equation #linear #quantifier: A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations (AKJ, SC), pp. 486–503.
CAV-2011-JoseM #fault #locality #named #source code: Bug-Assist: Assisting Fault Localization in ANSI-C Programs (MJ, RM), pp. 504–509.
CAV-2011-KatzPS #distributed #synthesis: Synthesis of Distributed Control through Knowledge Accumulation (GK, DP, SS), pp. 510–525.
CAV-2011-KieferMOWW #automaton #equivalence #probability: Language Equivalence for Probabilistic Automata (SK, ASM, JO, BW, JW), pp. 526–540.
CAV-2011-KleinN #automation #behaviour #formal method #rest #verification: Formalization and Automated Verification of RESTful Behavior (UK, KSN), pp. 541–556.
CAV-2011-KroeningOSWW #bound #linear #model checking: Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
CAV-2011-KroeningW #verification: Interpolation-Based Software Verification with Wolverine (DK, GW), pp. 573–578.
CAV-2011-KuglerPR #biology: Synthesizing Biological Theories (HK, CP, AR), pp. 579–584.
CAV-2011-KwiatkowskaNP #probability #realtime #verification: PRISM 4.0: Verification of Probabilistic Real-Time Systems (MZK, GN, DP), pp. 585–591.
CAV-2011-LeeYP #data type #program analysis: Program Analysis for Overlaid Data Structures (OL, HY, RP), pp. 592–608.
CAV-2011-LiGR #automation #c++ #execution #generative #named #source code #symbolic computation #testing: KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs (GL, IG, SPR), pp. 609–615.
CAV-2011-MorbePS #automaton #model checking: Fully Symbolic Model Checking for Timed Automata (GM, FP, CS), pp. 616–632.
CAV-2011-MullerP #hardware #interface #verification: Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus (CAM, WJP), pp. 633–648.
CAV-2011-PeterEM #automaton #named #synthesis #verification: Synthia: Verification and Synthesis for Timed Automata (HJP, RE, RM), pp. 649–655.
CAV-2011-PhamTTC #constraints #fixpoint #named #quantifier: FixBag: A Fixpoint Calculator for Quantified Bag Constraints (THP, MTT, AHT, WNC), pp. 656–662.
CAV-2011-RamanK #behaviour #specification #using: Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP (VR, HKG), pp. 663–668.
CAV-2011-RamosE #equivalence #verification: Practical, Low-Effort Equivalence Verification of Real Code (DAR, DRE), pp. 669–685.
CAV-2011-SankaranarayananT #abstraction #hybrid #relational: Relational Abstractions for Continuous and Hybrid Systems (SS, AT), pp. 686–702.
CAV-2011-SharmaDDA #generative #invariant #using: Simplifying Loop Invariant Generation Using Splitter Predicates (RS, ID, TD, AA), pp. 703–719.
CAV-2011-SistlaZF #probability: Monitorability of Stochastic Dynamical Systems (APS, MZ, YF), pp. 720–736.
CAV-2011-SteppTL #validation: Equality-Based Translation Validator for LLVM (MS, RT, SL), pp. 737–742.
CAV-2011-HagueL #data type #model checking #recursion #source code: Model Checking Recursive Programs with Numeric Data Types (MH, AWL), pp. 743–759.

Ganesh Gopalakrishnan, Shaz QadeerProceedings of the 23rd International Conference on Computer Aided VerificationCAV, 2011.

Contents (60 items)

Ganesh Gopalakrishnan, Shaz Qadeer
Proceedings of the 23rd International Conference on Computer Aided Verification
CAV, 2011.