000 03897nam a22005415i 4500
001 978-3-540-69738-1
003 DE-He213
005 20240730191025.0
007 cr nn 008mamaa
008 100301s2007 gw | s |||| 0|eng d
020 _a9783540697381
_9978-3-540-69738-1
024 7 _a10.1007/978-3-540-69738-1
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
072 7 _aUMZ
_2thema
082 0 4 _a005.1
_223
245 1 0 _aVerification, Model Checking, and Abstract Interpretation
_h[electronic resource] :
_b8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings /
_cedited by Byron Cook, Andreas Podelski.
250 _a1st ed. 2007.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2007.
300 _aXI, 395 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v4349
505 0 _aInvited Talk -- DIVINE: DIscovering Variables IN Executables -- Session 1 -- Verifying Compensating Transactions -- Model Checking Nonblocking MPI Programs -- Model Checking Via ?CFA -- Using First-Order Theorem Provers in the Jahob Data Structure Verification System -- Invited Tutorial -- Interpolants and Symbolic Model Checking -- Session 2 -- Shape Analysis of Single-Parent Heaps -- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures -- On Flat Programs with Lists -- Invited Talk -- Automata-Theoretic Model Checking Revisited -- Session 3 -- Language-Based Abstraction Refinement for Hybrid System Verification -- More Precise Partition Abstractions -- The Spotlight Principle -- Lattice Automata -- Invited Tutorial -- Learning Algorithms and Formal Verification (Invited Tutorial) -- Session 4 -- Constructing Specialized Shape Analyses for Uniform Change -- Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning -- Automated Verification of Shape and Size Properties Via Separation Logic -- Invited Talk -- Towards Shape Analysis for Device Drivers -- Session 5 -- An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints -- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes -- Symmetry and Completeness in the Analysis of Parameterized Systems -- Better Under-Approximation of Programs by Hiding Variables -- Invited Tutorial -- The Constraint Database Approach to Software Verification -- Session 6 -- Constraint Solving for Interpolation -- Assertion Checking Unified -- Invariant Synthesis for Combined Theories.
650 0 _aSoftware engineering.
_94138
650 0 _aComputer science.
_99832
650 0 _aCompilers (Computer programs).
_93350
650 1 4 _aSoftware Engineering.
_94138
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aCompilers and Interpreters.
_931853
700 1 _aCook, Byron.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9144897
700 1 _aPodelski, Andreas.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9144898
710 2 _aSpringerLink (Online service)
_9144899
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540697350
776 0 8 _iPrinted edition:
_z9783540834823
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v4349
_9144900
856 4 0 _uhttps://doi.org/10.1007/978-3-540-69738-1
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c93581
_d93581