000 03675nam a22005295i 4500
001 978-3-540-31899-6
003 DE-He213
005 20240423125955.0
007 cr nn 008mamaa
008 100723s2005 gw | s |||| 0|eng d
020 _a9783540318996
_9978-3-540-31899-6
024 7 _a10.1007/11537328
_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 _aModel Checking Software
_h[electronic resource] :
_b12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings /
_cedited by Patrick Godefroid.
250 _a1st ed. 2005.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2005.
300 _aXII, 292 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 ;
_v3639
505 0 _aInvited Talks/Papers -- Pushdown Model Checking for Security -- Execution Generated Test Cases: How to Make Systems Code Crash Itself -- Invited Tutorials -- Effective Bug Hunting with Spin and Modex -- The BLAST Software Verification System -- Model Checking Programs with Java PathFinder -- State Representation and Abstraction -- An Incremental Heap Canonicalization Algorithm -- Memory Efficient State Space Storage in Explicit Software Model Checking -- Counterexample-Based Refinement for a Boundedness Test for CFSM Languages -- Dealing with Concurrency -- Symbolic Model Checking for Asynchronous Boolean Programs -- Improving Spin’s Partial-Order Reduction for Breadth-First Search -- Sound Transaction-Based Reduction Without Cycle Detection -- Dealing with Complex Data -- Repairing Structurally Complex Data -- Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices -- Behavioural Models for Hierarchical Components -- Checking Temporal Properties -- On-the-Fly Emptiness Checks for Generalized Büchi Automata -- Stuttering Congruence for ? -- Verifying Pattern-Generated LTL Formulas: A Case Study -- Checking Security and Real-Time Properties -- Generic Verification of Security Protocols -- Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models -- Model Checking Machine Code with the GNU Debugger -- Tool Papers -- Etch: An Enhanced Type Checking Tool for Promela -- Enhanced Probabilistic Verification with 3Spin and 3Murphi -- SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions -- Learning-Based Assume-Guarantee Verification (Tool Paper).
650 0 _aSoftware engineering.
650 0 _aCompilers (Computer programs).
650 0 _aComputer science.
650 1 4 _aSoftware Engineering.
650 2 4 _aCompilers and Interpreters.
650 2 4 _aComputer Science Logic and Foundations of Programming.
700 1 _aGodefroid, Patrick.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540281955
776 0 8 _iPrinted edition:
_z9783540814030
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v3639
856 4 0 _uhttps://doi.org/10.1007/11537328
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c183675
_d183675