LEADER 03434nam 2200541 a 450 001 9910482992703321 005 20200520144314.0 010 $a3-540-31622-1 024 7 $a10.1007/11609773 035 $a(CKB)1000000000213581 035 $a(SSID)ssj0000320628 035 $a(PQKBManifestationID)11235359 035 $a(PQKBTitleCode)TC0000320628 035 $a(PQKBWorkID)10258633 035 $a(PQKB)10449851 035 $a(DE-He213)978-3-540-31622-0 035 $a(MiAaPQ)EBC3068420 035 $a(PPN)123099153 035 $a(EXLCZ)991000000000213581 100 $a20051129d2006 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aVerification, model checking, and abstract interpretation $e7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006 : proceedings /$fE. Allen Emerson, Kedar S. Namjoshi (eds.) 205 $a1st ed. 2006. 210 $aBerlin $cSpringer$d2006 215 $a1 online resource (XI, 443 p.) 225 1 $aLecture notes in computer science,$x0302-9743 ;$v3855 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-31139-4 320 $aIncludes bibliographical references and index. 327 $aClosure Operators for ROBDDs -- A CLP Method for Compositional and Intermittent Predicate Abstraction -- Combining Shape Analyses by Intersecting Abstractions -- A Complete Abstract Interpretation Framework for Coverability Properties of WSTS -- Complexity Results on Branching-Time Pushdown Model Checking -- A Compositional Logic for Control Flow -- Detecting Non-cyclicity by Abstract Compilation into Boolean Functions -- Efficient Strongly Relational Polyhedral Analysis -- Environment Abstraction for Parameterized Verification -- Error Control for Probabilistic Model Checking -- Field Constraint Analysis -- A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety -- Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems -- A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs -- Monitoring Off-the-Shelf Components -- Parallel External Directed Model Checking with Linear I/O -- Piecewise FIFO Channels Are Analyzable -- Ranking Abstraction of Recursive Programs -- Relative Safety -- Resource Usage Analysis for the ?-Calculus -- Semantic Hierarchy Refactoring by Abstract Interpretation -- Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation -- Symbolic Methods to Enhance the Precision of Numerical Abstract Domains -- Synthesis of Reactive(1) Designs -- Systematic Construction of Abstractions for Model-Checking -- Totally Clairvoyant Scheduling with Relative Timing Constraints -- Verification of Well-Formed Communicating Recursive State Machines -- What?s Decidable About Arrays?. 410 0$aLecture notes in computer science ;$v3855. 517 3 $aVMCAI 2006 606 $aComputer programs$xVerification$vCongresses 615 0$aComputer programs$xVerification 676 $a005.14 701 $aEmerson$b E. Allen$01756345 701 $aNamjoshi$b Kedar S$01756346 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910482992703321 996 $aVerification, model checking, and abstract interpretation$94193578 997 $aUNINA