03973nam 22007455 450 99646598630331620230222085607.01-280-38959-197866135675123-642-16164-210.1007/978-3-642-16164-3(CKB)2670000000045146(SSID)ssj0000446632(PQKBManifestationID)11249946(PQKBTitleCode)TC0000446632(PQKBWorkID)10511801(PQKB)11624140(DE-He213)978-3-642-16164-3(MiAaPQ)EBC3065903(PPN)149025300(EXLCZ)99267000000004514620100920d2010 u| 0engurnn|008mamaatxtccrModel Checking Software[electronic resource] 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings /edited by Jaco van der Pol, Michael Weber1st ed. 2010.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2010.1 online resource (X, 263 p. 70 illus.) Theoretical Computer Science and General Issues,2512-2029 ;6349Bibliographic Level Mode of Issuance: Monograph3-642-16163-4 Includes bibliographical references and index.Satisfiability 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.Theoretical Computer Science and General Issues,2512-2029 ;6349Software engineeringCompilers (Computer programs)Computer programmingComputer scienceMachine theorySoftware EngineeringCompilers and InterpretersProgramming TechniquesComputer Science Logic and Foundations of ProgrammingFormal Languages and Automata TheorySoftware engineering.Compilers (Computer programs).Computer programming.Computer science.Machine theory.Software Engineering.Compilers and Interpreters.Programming Techniques.Computer Science Logic and Foundations of Programming.Formal Languages and Automata Theory.005.1van der Pol Jacoedthttp://id.loc.gov/vocabulary/relators/edtWeber Michaeledthttp://id.loc.gov/vocabulary/relators/edtInternational SPIN WorkshopBOOK996465986303316Model Checking Software771961UNISA