LEADER 03959nam 22007215 450 001 9910484349603321 005 20251226200000.0 010 $a3-540-73370-1 024 7 $a10.1007/978-3-540-73370-6 035 $a(CKB)1000000000490800 035 $a(SSID)ssj0000318968 035 $a(PQKBManifestationID)11224891 035 $a(PQKBTitleCode)TC0000318968 035 $a(PQKBWorkID)10336587 035 $a(PQKB)10554965 035 $a(DE-He213)978-3-540-73370-6 035 $a(MiAaPQ)EBC3061725 035 $a(MiAaPQ)EBC6698664 035 $a(Au-PeEL)EBL6698664 035 $a(PPN)12316334X 035 $a(BIP)34164894 035 $a(BIP)14225060 035 $a(EXLCZ)991000000000490800 100 $a20100301d2007 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aModel Checking Software $e14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings /$fedited by Dragan Bosnacki, Stefan Edelkamp 205 $a1st ed. 2007. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007. 215 $a1 online resource (X, 285 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4595 300 $a"Collocated with CAV 2007, the 19th Computer-Aided Verification Conference"-- Pref. 311 08$a3-540-73369-8 320 $aIncludes bibliographical references and index. 327 $aStackSnuffer: Curing Orion?s Unsoundness -- Tutorial: Parallel Model Checking -- Local Abstraction-Refinement for the mu-Calculus -- Minimal Counterexample Generation for SPIN -- Generating Counter-Examples Through Randomized Guided Search -- Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software -- Some Solutions to the Ignoring Problem -- Cartesian Partial-Order Reduction -- On-the-Fly Dynamic Dead Variable Analysis -- SAT-Based Summarization for Boolean Programs -- LTL Satisfiability Checking -- An Embeddable Virtual Machine for State Space Generation -- Scalable Multi-core LTL Model-Checking -- A SystemC/TLM Semantics in Promela and Its Possible Applications -- Towards Model Checking Spatial Properties with SPIN -- Model Extraction for ARINC 653 Based Avionics Software -- BEEM: Benchmarks for Explicit Model Checkers -- C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs -- ACSAR: Software Model Checking with Transfinite Refinement -- Instrumenting C Programs with Nested Word Monitors. 330 $aThis book presents the proceedings of the 14th International SPIN workshop on Model Checking Software, held in Berlin, Germany. Fourteen full papers are presented, together with four tool presentation papers and the abstracts of two invited talks. The papers are organized into topical sections covering directed model checking, partial order reduction, program analysis, exploration advances, modeling and case studies, and tool demonstrations. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4595 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aComputer science 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer Science Logic and Foundations of Programming 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aComputer science. 615 14$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer Science Logic and Foundations of Programming. 676 $a005.1/4 702 $aBos?nac?ki$b Dragan$f1963- 702 $aEdelkamp$b Stefan 712 12$aCAV (Conference)$d(19th :$f2007 :$eBerlin, Germany) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484349603321 996 $aModel Checking Software$93359484 997 $aUNINA