06099nam 2200625 a 450 991048295890332120200520144314.01-280-38785-897866135657783-642-14295-810.1007/978-3-642-14295-6(CKB)2550000000015596(SSID)ssj0000446364(PQKBManifestationID)11297669(PQKBTitleCode)TC0000446364(PQKBWorkID)10492148(PQKB)10580752(DE-He213)978-3-642-14295-6(MiAaPQ)EBC3065505(PPN)149072821(EXLCZ)99255000000001559620100601d2010 uy 0engurnn|008mamaatxtccrComputer aided verification 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 : proceedings /Tayssir Touili, Byron Cook, Paul Jackson (eds.)1st ed. 2010.New York Springer20101 online resource (XVI, 676 p. 169 illus.) Lecture notes in computer science,0302-9743 ;6174LNCS sublibrary. SL 1, Theoretical computer science and general issuesBibliographic Level Mode of Issuance: Monograph3-642-14294-X Includes bibliographical references and index.Invited Talks -- Policy Monitoring in First-Order Temporal Logic -- Retrofitting Legacy Code for Security -- Quantitative Information Flow: From Theory to Practice? -- Memory Management in Concurrent Algorithms -- Invited Tutorials -- ABC: An Academic Industrial-Strength Verification Tool -- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code -- Constraint Solving for Program Verification: Theory and Practice by Example -- Session 1. Software Model Checking -- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data -- Termination Analysis with Compositional Transition Invariants -- Lazy Annotation for Program Testing and Verification -- The Static Driver Verifier Research Platform -- Dsolve: Safety Verification via Liquid Types -- Contessa: Concurrency Testing Augmented with Symbolic Analysis -- Session 2. Model Checking and Automata -- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing -- Efficient Emptiness Check for Timed Büchi Automata -- Session 3. Tools -- Merit: An Interpolating Model-Checker -- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems -- Jtlv: A Framework for Developing Verification Algorithms -- Petruchio: From Dynamic Networks to Nets -- Session 4. Counter and Hybrid Systems Verification -- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems -- Safety Verification for Probabilistic Hybrid Systems -- A Logical Product Approach to Zonotope Intersection -- Fast Acceleration of Ultimately Periodic Relations -- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks -- Session 5. Memory Consistency -- Fences in Weak Memory Models -- Generating Litmus Tests for Contrasting Memory Consistency Models -- Session 6. Verification of Hardware and Low Level Code -- Directed Proof Generation for Machine Code -- Verifying Low-Level Implementations of High-Level Datatypes -- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics -- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification -- Session 7. Tools -- LTSmin: Distributed and Symbolic Reachability -- libalf: The Automata Learning Framework -- Session 8. Synthesis -- Symbolic Bounded Synthesis -- Measuring and Synthesizing Systems in Probabilistic Environments -- Achieving Distributed Control through Model Checking -- Robustness in the Presence of Liveness -- RATSY – A New Requirements Analysis Tool with Synthesis -- Comfusy: A Tool for Complete Functional Synthesis -- Session 9. Concurrent Program Verification I -- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs -- Automatically Proving Linearizability -- Model Checking of Linearizability of Concurrent List Implementations -- Local Verification of Global Invariants in Concurrent Programs -- Abstract Analysis of Symbolic Executions -- Session 10. Compositional Reasoning -- Automated Assume-Guarantee Reasoning through Implicit Learning -- Learning Component Interfaces with May and Must Abstractions -- A Dash of Fairness for Compositional Reasoning -- SPLIT: A Compositional LTL Verifier -- Session 11. Tools -- A Model Checker for AADL -- PESSOA: A Tool for Embedded Controller Synthesis -- Session 12. Decision Procedures -- On Array Theory of Bounded Elements -- Quantifier Elimination by Lazy Model Enumeration -- Session 13. Concurrent Program Verification II -- Bounded Underapproximations -- Global Reachability in Bounded Phase Multi-stack Pushdown Systems -- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces -- Dynamic Cutoff Detection in Parameterized Concurrent Programs -- Session 14. Tools -- PARAM: A Model Checker for Parametric Markov Models -- Gist: A Solver for Probabilistic Games -- A NuSMV Extension for Graded-CTL Model Checking.Lecture notes in computer science ;6174.LNCS sublibrary.SL 1,Theoretical computer science and general issues.CAV 2010Computer softwareVerificationCongressesIntegrated circuitsVerificationCongressesComputer softwareVerificationIntegrated circuitsVerification005.1015113Touili Tayssir1762734Cook Byron1758373Jackson Paul291525MiAaPQMiAaPQMiAaPQBOOK9910482958903321Computer aided verification4202846UNINA