Proceedings of the 23rd 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

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

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

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.