LEADER 04212nam 2200553Ia 450 001 9910484590103321 005 20200520144314.0 010 $a3-540-93900-8 024 7 $a10.1007/978-3-540-93900-9 035 $a(CKB)1000000000545922 035 $a(SSID)ssj0000320627 035 $a(PQKBManifestationID)11937793 035 $a(PQKBTitleCode)TC0000320627 035 $a(PQKBWorkID)10249731 035 $a(PQKB)10561021 035 $a(DE-He213)978-3-540-93900-9 035 $a(MiAaPQ)EBC3063865 035 $a(PPN)132869004 035 $a(EXLCZ)991000000000545922 100 $a20081208d2009 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aVerification, model checking, and abstract interpretation $e10th international conference, VMCAI 2009, Savannah, GA, USA, January 18 - 20, 2009 ; proceedings /$fNeil D. Jones, Markus Muller-Olm (eds.) 205 $a1st ed. 2009. 210 $aNew York, NY ;$aBerlin ;$aHeidelberg $cSpringer$dc2009 215 $a1 online resource (XI, 381 p.) 225 1 $aLecture notes in computer science ;$vv. 5403 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-93899-0 327 $aInvited Talks -- Model Checking: Progress and Problems -- Model Checking Concurrent Programs -- Thread-Modular Shape Analysis -- Invited Tutorials -- Advances in Program Termination and Liveness -- Verification of Security Protocols -- Submitted Papers -- Towards Automatic Stability Analysis for Rely-Guarantee Proofs -- Mostly-Functional Behavior in Java Programs -- The Higher-Order Aggregate Update Problem -- An Abort-Aware Model of Transactional Programming -- Model-Checking the Linux Virtual File System -- LTL Generalized Model Checking Revisited -- Monitoring the Full Range of ?-Regular Properties of Stochastic Systems -- Constraint-Based Invariant Inference over Predicate Abstraction -- Reducing Behavioural to Structural Properties of Programs with Procedures -- Query-Driven Program Testing -- Average-Price-per-Reward Games on Hybrid Automata with Strong Resets -- Abstraction Refinement for Probabilistic Software -- Finding Concurrency-Related Bugs Using Random Isolation -- An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries -- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities -- Deciding Extensions of the Theories of Vectors and Bags -- A Posteriori Soundness for Non-deterministic Abstract Interpretations -- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking -- A Scalable Memory Model for Low-Level Code -- Synthesizing Switching Logic Using Constraint Solving -- Extending Symmetry Reduction by Exploiting System Architecture -- Shape-Value Abstraction for Verifying Linearizability -- Mixed Transition Systems Revisited -- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. 330 $aThe book constitutes the refereed proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2009, held in Savannah, GA, USA, in January 2009 - co-located with POPL 2009, the 36th Annual Symposium on Principles of Programming Languages. The 24 revised full papers presented together with 3 invited talks and 2 invited tutorials were carefully reviewed and selected from 72 submissions. The papers address all current issues from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine the three areas. 410 0$aLecture notes in computer science ;$v5403. 606 $aMathematical optimization 606 $aProgramming (Mathematics) 615 0$aMathematical optimization. 615 0$aProgramming (Mathematics) 676 $a005.11 701 $aJones$b Neil D$059760 701 $aMuller-Olm$b Markus$0508822 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484590103321 996 $aVerification, model checking, and abstract interpretation$94193177 997 $aUNINA