000 03438nam a22004815i 4500
001 978-3-540-31899-6
003 DE-He213
005 20160624101919.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
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 Patrice Godefroid.
260 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_c2005.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_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 _aLecture Notes in Computer Science,
_x0302-9743 ;
_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 _aComputer science.
650 0 _aSoftware engineering.
650 0 _aLogic design.
650 1 4 _aComputer Science.
650 2 4 _aSoftware Engineering.
650 2 4 _aProgramming Languages, Compilers, Interpreters.
650 2 4 _aLogics and Meanings of Programs.
700 1 _aGodefroid, Patrice.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783540281955
786 _dSpringer
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v3639
856 4 0 _uhttp://dx.doi.org/10.1007/11537328
942 _2EBK3700
_cEBK
999 _c32994
_d32994