Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings (Lecture Notes in Computer Science, 6174)

Annotation This book constitutes the refereed proceedings of the 22nd International Conference on Computer Aided Verification, CAV 2010, held in Edinburgh, UK, in July 2010 as part of the Federated Logic Conference, FLoC 2010. The 34 revised full papers presented together with 17 tool papers, 4 invited talks and 3 invited tutorials were carefully reviewed and selected from 101 regular paper and 44 tool paper submissions. The papers are dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for hardware and software systems. They are organized in topical sections on software model checking; model checking and automata; tools; counter and hybrid systems verification; memory consistency; verification of hardware and low level code; synthesis; concurrent program verification; compositional reasoning; and decision procedures Front Matter....Pages - Policy Monitoring in First-Order Temporal Logic....Pages 1-18 Retrofitting Legacy Code for Security....Pages 19-19 Quantitative Information Flow: From Theory to Practice?....Pages 20-22 Memory Management in Concurrent Algorithms....Pages 23-23 ABC: An Academic Industrial-Strength Verification Tool....Pages 24-40 There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code....Pages 41-56 Constraint Solving for Program Verification: Theory and Practice by Example....Pages 57-71 Invariant Synthesis for Programs Manipulating Lists with Unbounded Data....Pages 72-88 Termination Analysis with Compositional Transition Invariants....Pages 89-103 Lazy Annotation for Program Testing and Verification....Pages 104-118 The Static Driver Verifier Research Platform....Pages 119-122 Dsolve: Safety Verification via Liquid Types....Pages 123-126 Contessa : Concurrency Testing Augmented with Symbolic Analysis....Pages 127-131 Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing....Pages 132-147 Efficient Emptiness Check for Timed Büchi Automata....Pages 148-161 Merit : An Interpolating Model-Checker....Pages 162-166 Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems....Pages 167-170 Jtlv : A Framework for Developing Verification Algorithms....Pages 171-174 Petruchio: From Dynamic Networks to Nets....Pages 175-179 Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems....Pages 180-195 Safety Verification for Probabilistic Hybrid Systems....Pages 196-211 A Logical Product Approach to Zonotope Intersection....Pages 212-226 Fast Acceleration of Ultimately Periodic Relations....Pages 227-242 An Abstraction-Refinement Approach to Verification of Artificial Neural Networks....Pages 243-257 Fences in Weak Memory Models....Pages 258-272 Generating Litmus Tests for Contrasting Memory Consistency Models....Pages 273-287 Directed Proof Generation for Machine Code....Pages 288-305 Verifying Low-Level Implementations of High-Level Datatypes....Pages 306-320 Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics....Pages 321-338 Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification....Pages 339-353 LTSmin: Distributed and Symbolic Reachability....Pages 354-359 libalf : The Automata Learning Framework....Pages 360-364 Symbolic Bounded Synthesis....Pages 365-379 Measuring and Synthesizing Systems in Probabilistic Environments....Pages 380-395 Achieving Distributed Control through Model Checking....Pages 396-409 Robustness in the Presence of Liveness....Pages 410-424 RATSY – A New Requirements Analysis Tool with Synthesis....Pages 425-429 Comfusy : A Tool for Complete Functional Synthesis....Pages 430-433 Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs....Pages 434-449 Automatically Proving Linearizability....Pages 450-464 Model Checking of Linearizability of Concurrent List Implementations....Pages 465-479 Local Verification of Global Invariants in Concurrent Programs....Pages 480-494 Abstract Analysis of Symbolic Executions....Pages 495-510 Automated Assume-Guarantee Reasoning through Implicit Learning....Pages 511-526 Learning Component Interfaces with May and Must Abstractions....Pages 527-542 A Dash of Fairness for Compositional Reasoning....Pages 543-557 SPLIT: A Compositional LTL Verifier....Pages 558-561 A Model Checker for AADL....Pages 562-565 PESSOA: A Tool for Embedded Controller Synthesis....Pages 566-569 On Array Theory of Bounded Elements....Pages 570-584 Quantifier Elimination by Lazy Model Enumeration....Pages 585-599 Bounded Underapproximations....Pages 600-614 Global Reachability in Bounded Phase Multi-stack Pushdown Systems....Pages 615-628 Model-Checking Parameterized Concurrent Programs Using Linear Interfaces....Pages 629-644 Dynamic Cutoff Detection in Parameterized Concurrent Programs....Pages 645-659 PARAM : A Model Checker for Parametric Markov Models....Pages 660-664 Gist : A Solver for Probabilistic Games....Pages 665-669 A NuSMV Extension for Graded-CTL Model Checking....Pages 670-673 Back Matter....Pages -