LEADER 04248nam 2200649Ia 450 001 9910484667803321 005 20200520144314.0 010 $a1-280-38541-3 010 $a9786613563330 010 $a3-642-11319-2 024 7 $a10.1007/978-3-642-11319-2 035 $a(CKB)2670000000003403 035 $a(SSID)ssj0000355650 035 $a(PQKBManifestationID)11249124 035 $a(PQKBTitleCode)TC0000355650 035 $a(PQKBWorkID)10340829 035 $a(PQKB)10411257 035 $a(DE-He213)978-3-642-11319-2 035 $a(MiAaPQ)EBC3064942 035 $a(PPN)149054866 035 $a(Association for Computing Machinery)10.5555/2127753 035 $a(EXLCZ)992670000000003403 100 $a20091127d2010 uy 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aVerification, model checking, and abstract interpretation $e11th international conference, VMCAI 2010 ; Madrid, Spain, January 17-19, 2010 ; proceedings /$fGilles Barthe, Manuel Hermenegildo (eds.) 205 $a1st ed. 2010. 210 $aBerlin $cSpringer$dc2010 215 $a1 online resource (X, 397 p.) 225 1 $aLecture notes in computer science,$x0302-9743 ;$v5944 225 1 $aLNCS sublibrary. SL 1, Theoretical computer science and general issues 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-11318-4 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Analysis of Systems with Stochastic Process Creation -- Verifying Concurrent Programs with Chalice -- Static Timing Analysis for Hard Real-Time Systems -- Invited Tutorials -- Abstract Interpretation-Based Protection -- Advances in Probabilistic Model Checking -- Building a Calculus of Data Structures -- Regular Papers -- Temporal Reasoning for Procedural Programs -- Improved Model Checking of Hierarchical Systems -- Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming -- Complexity Bounds for the Verification of Real-Time Software -- An Abstract Domain to Discover Interval Linear Equalities -- Interpolant Strength -- Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing -- Invariant and Type Inference for Matrices -- Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction -- Automatic Abstraction for Congruences -- Shape Analysis of Low-Level C with Overlapping Structures -- Abstract Threads -- Shape Analysis with Reference Set Relations -- Shape Analysis in the Absence of Pointers and Structure -- An Analysis of Permutations in Arrays -- Regular Linear Temporal Logic with Past -- Model-Checking In-Lined Reference Monitors -- Considerate Reasoning and the Composite Design Pattern -- RGSep Action Inference -- Best Probabilistic Transformers -- Collections, Cardinalities, and Relations. 330 $aThis book constitutes the refereed proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010, held in Madrid, Spain, in January 2010. The 21 papers included in this volume were carefully reviewed and selected from 57 submissions. In addition 3 invited talks and 3 invited tutorials are presented. Topics covered by VMCAI include program verification, program certification, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. 410 0$aLecture notes in computer science ;$v5944. 410 0$aLNCS sublibrary.$nSL 1,$pTheoretical computer science and general issues. 517 3 $aVMCAI 2010 606 $aComputer programs$xVerification$vCongresses 606 $aComputer science 615 0$aComputer programs$xVerification 615 0$aComputer science. 676 $a005.1 701 $aBarthe$b Gilles$f1967-$0180568 701 $aHermenegildo$b Manuel$0971279 712 12$aVMCAI 2010 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484667803321 996 $aVerification, model checking, and abstract interpretation$94200350 997 $aUNINA