Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings

Front Matter....Pages -
HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection....Pages 1-19
Using Types for Software Verification....Pages 20-20
SMT-Based Modular Analysis of Sequential Systems Code....Pages 21-27
Logic and Compositional Verification of Hybrid Systems....Pages 28-43
Using Coverage to Deploy Formal Verification in a Simulation World....Pages 44-49
Stability in Weak Memory Models....Pages 50-66
Verification of Certifying Computations....Pages 67-82
Parameter Identification for Markov Models of Biochemical Reactions....Pages 83-98
Getting Rid of Store-Buffers in TSO Analysis....Pages 99-115
Malware Analysis with Tree Automata Inference....Pages 116-131
State/Event-Based LTL Model Checking under Parametric Generalized Fairness....Pages 132-148
Resolution Proofs and Skolem Functions in QBF Evaluation and Applications....Pages 149-164
The BINCOA Framework for Binary Code Analysis....Pages 165-170
CVC4....Pages 171-177
 SLAyer : Memory Safety for Systems-Level Code....Pages 178-183
 CPAchecker : A Tool for Configurable Software Verification....Pages 184-190
Existential Quantification as Incremental SAT....Pages 191-207
Efficient Analysis of Probabilistic Programs with an Unbounded Counter....Pages 208-224
Model Checking Algorithms for CTMDPs....Pages 225-242
Quantitative Synthesis for Concurrent Programs....Pages 243-259
Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives....Pages 260-276
Smoothing a Program Soundly and Robustly....Pages 277-292
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification....Pages 293-309
 Kratos – A Software Model Checker for SystemC....Pages 310-316
Efficient Scenario Verification for Hybrid Automata....Pages 317-332
Temporal Property Verification as a Program Analysis Task....Pages 333-348
Time for Statistical Model Checking of Real-Time Systems....Pages 349-355
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs....Pages 356-371
Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic....Pages 372-378
SpaceEx: Scalable Verification of Hybrid Systems....Pages 379-395
From Cardiac Cells to Genetic Regulatory Networks....Pages 396-411
Threader: A Constraint-Based Verifier for Multi-threaded Programs....Pages 412-417
Interactive Synthesis of Code Snippets....Pages 418-423
Forest Automata for Verification of Heap Manipulation....Pages 424-440
Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints....Pages 441-456
 μZ – An Efficient Engine for Fixed Points with Constraints....Pages 457-462
BAP: A Binary Analysis Platform....Pages 463-469
HMC: Verifying Functional Programs Using Abstract Interpreters....Pages 470-485
A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations....Pages 486-503
Bug-Assist: Assisting Fault Localization in ANSI-C Programs....Pages 504-509
Synthesis of Distributed Control through Knowledge Accumulation....Pages 510-525
Language Equivalence for Probabilistic Automata....Pages 526-540
Formalization and Automated Verification of RESTful Behavior....Pages 541-556
Linear Completeness Thresholds for Bounded Model Checking....Pages 557-572
Interpolation-Based Software Verification with Wolverine ....Pages 573-578
Synthesizing Biological Theories....Pages 579-584
PRISM 4.0: Verification of Probabilistic Real-Time Systems....Pages 585-591
Program Analysis for Overlaid Data Structures....Pages 592-608
KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs....Pages 609-615
Fully Symbolic Model Checking for Timed Automata....Pages 616-632
Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus....Pages 633-648
Synthia: Verification and Synthesis for Timed Automata....Pages 649-655
 FixBag : A Fixpoint Calculator for Quantified Bag Constraints....Pages 656-662
Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP....Pages 663-668
Practical, Low-Effort Equivalence Verification of Real Code....Pages 669-685
Relational Abstractions for Continuous and Hybrid Systems....Pages 686-702
Simplifying Loop Invariant Generation Using Splitter Predicates....Pages 703-719
Monitorability of Stochastic Dynamical Systems....Pages 720-736
Equality-Based Translation Validator for LLVM....Pages 737-742
Model Checking Recursive Programs with Numeric Data Types....Pages 743-759
Back Matter....Pages -