LEADER 03973nam  22007455  450 
001 996465986303316
005 20230222085607.0
010   $a1-280-38959-1
010   $a9786613567512
010   $a3-642-16164-2
024 7 $a10.1007/978-3-642-16164-3
035   $a(CKB)2670000000045146
035   $a(SSID)ssj0000446632
035   $a(PQKBManifestationID)11249946
035   $a(PQKBTitleCode)TC0000446632
035   $a(PQKBWorkID)10511801
035   $a(PQKB)11624140
035   $a(DE-He213)978-3-642-16164-3
035   $a(MiAaPQ)EBC3065903
035   $a(PPN)149025300
035   $a(EXLCZ)992670000000045146
100   $a20100920d2010      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aModel Checking Software$b[electronic resource] $e17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings /$fedited by Jaco van der Pol, Michael Weber
205   $a1st ed. 2010.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010.
215   $a1 online resource (X, 263 p. 70 illus.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6349
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-642-16163-4 
320   $aIncludes bibliographical references and index.
327   $aSatisfiability Modulo Theories for Model Checking -- SMT-Based Software Model Checking -- Symbolic Object Code Analysis -- Model Checking in Context -- Experimental Comparison of Concolic and Random Testing for Java Card Applets -- Combining SPIN with ns-2 for Protocol Optimization -- Automatic Generation of Model Checking Scripts Based on Environment Modeling -- Implementation and Performance of Model Checking -- Model Checking: Cleared for Take Off -- Context-Enhanced Directed Model Checking -- Efficient Explicit-State Model Checking on General Purpose Graphics Processors -- The SpinJa Model Checker -- LTL and Büchi Automata -- On the Virtue of Patience: Minimizing Büchi Automata -- Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance -- Nevertrace Claims for Model Checking -- Infinite State Models -- A False History of True Concurrency: From Petri to Tools -- Analysing Mu-Calculus Properties of Pushdown Systems -- Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains -- An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models -- Concurrent Software -- Context-Bounded Translations for Concurrent Software: An Empirical Evaluation -- One Stack to Run Them All.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v6349
606   $aSoftware engineering
606   $aCompilers (Computer programs)
606   $aComputer programming
606   $aComputer science
606   $aMachine theory
606   $aSoftware Engineering
606   $aCompilers and Interpreters
606   $aProgramming Techniques
606   $aComputer Science Logic and Foundations of Programming
606   $aFormal Languages and Automata Theory
615  0$aSoftware engineering.
615  0$aCompilers (Computer programs).
615  0$aComputer programming.
615  0$aComputer science.
615  0$aMachine theory.
615 14$aSoftware Engineering.
615 24$aCompilers and Interpreters.
615 24$aProgramming Techniques.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aFormal Languages and Automata Theory.
676   $a005.1
702   $avan der Pol$b Jaco$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aWeber$b Michael$4edt$4http://id.loc.gov/vocabulary/relators/edt
712 12$aInternational SPIN Workshop
906   $aBOOK
912   $a996465986303316
996   $aModel Checking Software$9771961
997   $aUNISA