LEADER 08624nam 22008535 450 001 9910482958903321 005 20251226202822.0 010 $a1-280-38785-8 010 $a9786613565778 010 $a3-642-14295-8 024 7 $a10.1007/978-3-642-14295-6 035 $a(CKB)2550000000015596 035 $a(SSID)ssj0000446364 035 $a(PQKBManifestationID)11297669 035 $a(PQKBTitleCode)TC0000446364 035 $a(PQKBWorkID)10492148 035 $a(PQKB)10580752 035 $a(DE-He213)978-3-642-14295-6 035 $a(MiAaPQ)EBC3065505 035 $a(PPN)149072821 035 $a(BIP)31063941 035 $a(EXLCZ)992550000000015596 100 $a20100709d2010 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aComputer Aided Verification $e22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings /$fedited by Tayssir Touili, Byron Cook, Paul Jackson 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (XVI, 676 p. 169 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6174 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-642-14294-X 320 $aIncludes bibliographical references and index. 327 $aInvited 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-LevelMicroarchitectural 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. 330 $aThis volume contains the proceedings of the 22nd International Conference on Computer-Aided Veri'cation (CAV) held in Edinburgh, UK, July 15-19 2010. CAV is dedicated to the advancement of the theory and practice of comput- assistedformalanalysismethods forsoftwareandhardwaresystems.Theconf- ence covers the spectrum from theoretical results to concrete applications, with an emphasis on practical veri'cation tools and the algorithms and techniques that are needed for their implementation. We received 145 submissions: 101 submissions of regular papers and 44 s- missions of tool papers. These submissions went through a meticulous review process;eachsubmissionwasreviewedbyatleast 4,andonaverage4.2 Program Committee members. Authors had the opportunity to respond to the initial - views during an author response period. This helped the Program Committee members to select 51 papers: 34 regular papers and 17 tool papers. In addition to the accepted papers, the program also included: - Five invited talks: * Policy Monitoring in First-Order Temporal Logic, by David Basin (ETH Zurich) * Retro'tting Legacy Code for Security, by Somesh Jha (University of Wisconsin-Madison) * Induction, Invariants, and Abstraction, by Deepak Kapur (University of New Mexico) * Quantitative Information Flow: From Theory to Practice? by Pasquale Malacaria (Queen Mary University) and * Memory Management in Concurrent Algorithms, by Maged Michael (IBM) - Four invited tutorials: * ABC: An Academic Industrial-Strength Veri'cation Tool, by Robert Brayton (University of California, Berkeley) * SoftwareModelChecking,byKennethMcMillan(CadenceBerkeleyLabs) * There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code, by Thomas Reps (University of Wisconsin-Madison) and 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6174 606 $aComputer science 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aMachine theory 606 $aArtificial intelligence 606 $aComputer networks 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aFormal Languages and Automata Theory 606 $aArtificial Intelligence 606 $aComputer Communication Networks 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aMachine theory. 615 0$aArtificial intelligence. 615 0$aComputer networks. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aFormal Languages and Automata Theory. 615 24$aArtificial Intelligence. 615 24$aComputer Communication Networks. 676 $a005.1015113 701 $aTouili$b Tayssir$01762734 701 $aCook$b Byron$01758373 701 $aJackson$b Paul$0291525 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910482958903321 996 $aComputer aided verification$94202846 997 $aUNINA