LEADER 04840nam 22006615 450 001 996465955603316 005 20230222133332.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 $a20100301d2009 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aVerification, Model Checking, and Abstract Interpretation$b[electronic resource] $e10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings /$fedited by Neil Jones, Markus Müller-Olm 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (XI, 381 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5403 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$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5403 606 $aComputer programming 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aComputer science 606 $aProgramming Techniques 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer Science Logic and Foundations of Programming 615 0$aComputer programming. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aComputer science. 615 14$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer Science Logic and Foundations of Programming. 676 $a005.11 702 $aJones$b Neil$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aMüller-Olm$b Markus$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465955603316 996 $aVerification, Model Checking, and Abstract Interpretation$92593983 997 $aUNISA