## Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, ProceedingsGanesh Gopalakrishnan, Shaz Qadeer This book constitutes the refereed proceedings of the 23rd International Conference on Computer Aided Verification, CAV 2011, held in Snowbird, UT, USA, in July 2011. The 35 revised full papers presented together with 20 tool papers were carefully reviewed and selected from 161 submissions. The papers are organized in topical sections on the following workshops: 4th International Workshop on Numerical Software Verification (NSV 2011), 10th International Workshop on Parallel and Distributed Methods in Verifications (PDMC 2011), 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 2011), Frontiers in Analog Circuit Synthesis and Verification (FAC 2011), International Workshop on Satisfiability Modulo Theories, including SMTCOMP (SMT 2011), 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), Formal Methods for Robotics and Automation (FM-R 2011), and Practical Synthesis for Concurrent Systems (PSY 2011). |

### Contents

1 | |

20 | |

21 | |

Logic and Compositional Verification of Hybrid Systems | 28 |

Using Coverage to Deploy Formal Verification in a Simulation World | 44 |

Stability in Weak Memory Models | 50 |

Verification of Certifying Computations | 67 |

Parameter Identification for Markov Models of Biochemical Reactions | 83 |

A ConstraintBased Verifier for Multithreaded Programs | 412 |

Interactive Synthesis of Code Snippets | 418 |

Forest Automata for Verification of Heap Manipulation | 424 |

Synthesizing CyberPhysical Architectural Models with RealTime Constraints | 441 |

μZ An Efficient Engine for Fixed Points with Constraints | 457 |

A Binary Analysis Platform | 463 |

Verifying Functional Programs Using Abstract Interpreters | 470 |

A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations | 486 |

Getting Rid of StoreBuffers in TSO Analysis | 99 |

Malware Analysis with Tree Automata Inference | 116 |

StateEventBased LTL Model Checking under Parametric Generalized Fairness | 132 |

Resolution Proofs and Skolem Functions in QBF Evaluation and Applications | 149 |

The BINCOA Framework for Binary Code Analysis | 165 |

CVC4 | 171 |

Memory Safety for SystemsLevel Code | 178 |

A Tool for Configurable Software Verification | 184 |

Existential Quantification as Incremental SAT | 191 |

EĈcient Analysis of Probabilistic Programs with an Unbounded Counter | 208 |

Model Checking Algorithms for CTMDPs | 225 |

Quantitative Synthesis for Concurrent Programs | 243 |

Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Buchi Objectives | 260 |

Smoothing a Program Soundly and Robustly | 277 |

A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification | 293 |

KRATOS A Software Model Checker for SystemC | 310 |

Efficient Scenario Verification for Hybrid Automata | 317 |

Temporal Property Verification as a Program Analysis Task | 333 |

Time for Statistical Model Checking of RealTime Systems | 349 |

SymmetryAware Predicate Abstraction for SharedVariable Concurrent Programs | 356 |

A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic | 372 |

Scalable Verification of Hybrid Systems | 379 |

From Cardiac Cells to Genetic Regulatory Networks | 396 |

Assisting Fault Localization in ANSIC Programs | 504 |

Synthesis of Distributed Control through Knowledge Accumulation | 510 |

Language Equivalence for Probabilistic Automata | 526 |

Formalization and Automated Verification of RESTful Behavior | 541 |

Linear Completeness Thresholds for Bounded Model Checking | 557 |

InterpolationBased Software Verification with Wolverine | 573 |

Synthesizing Biological Theories | 579 |

Verification of Probabilistic RealTime Systems | 585 |

Program Analysis for Overlaid Data Structures | 592 |

A Symbolic Execution and Automatic Test Generation Tool for C++ Programs | 609 |

Fully Symbolic Model Checking for Timed Automata | 616 |

Complete Formal Hardware Verification of Interfaces for a FlexRayLike Bus | 633 |

Verification and Synthesis for Timed Automata | 649 |

A Fixpoint Calculator for Quantified Bag Constraints | 656 |

Analyzing Unsynthesizable Specifications for HighLevel Robot Behavior Using LTLMoP | 663 |

Practical LowEffort Equivalence Verification of Real Code | 669 |

Relational Abstractions for Continuous and Hybrid Systems | 686 |

Simplifying Loop Invariant Generation Using Splitter Predicates | 703 |

Monitorability of Stochastic Dynamical Systems | 720 |

EqualityBased Translation Validator for LLVM | 737 |

Model Checking Recursive Programs with Numeric Data Types | 743 |

760 | |