LEADER 06438nam 22007455 450 001 9910143909703321 005 20251116234303.0 010 $a3-540-46017-9 024 7 $a10.1007/3-540-46017-9 035 $a(CKB)1000000000211714 035 $a(SSID)ssj0000324881 035 $a(PQKBManifestationID)11239175 035 $a(PQKBTitleCode)TC0000324881 035 $a(PQKBWorkID)10320517 035 $a(PQKB)10447808 035 $a(DE-He213)978-3-540-46017-6 035 $a(MiAaPQ)EBC3072057 035 $a(PPN)155211439 035 $a(EXLCZ)991000000000211714 100 $a20121227d2002 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aModel Checking Software $e9th International SPIN Workshop Grenoble, France, April 11-13, 2002 Proceedings /$fedited by Dragan Bosnacki, Stefan Leue 205 $a1st ed. 2002. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2002. 215 $a1 online resource (X, 262 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2318 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-43477-1 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- SAT-Based Counterexample Guided Abstraction Refinement -- Abstract Interpretation: Theory and Practice -- Invited Tutorial -- SPIN Tutorial: How to Become a SPIN Doctor -- Tutorial -- Abstraction in Software Model Checking: Principles and Practice -- Software Model Checking -- Symmetry Reduction Criteria for Software Model Checking -- Bytecode Model Checking: An Experimental Analysis -- The Influence of Software Module Systems on Modular Verification -- Extending the Translation from SDL to Promela -- Algorithms and Theoretical Foundations -- Model Checking Knowledge and Time -- Partial Order Reduction in Directed Model Checking -- Local Parallel Model Checking for the Alternation-Free ?-Calculus -- Applications -- The Agreement Problem Protocol Verification Environment -- Bottleneck Analysis of a Gigabit Network Interface Card: Formal Verification Approach -- Using SPIN to Verify Security Properties of Cryptographic Protocols -- Work in Progress -- Modeling and Verification of Interactive Flexible Multimedia Presentations Using PROMELA/SPIN -- SPINning Parallel Systems Software -- Dynamic Bounds and Transition Merging for Local First Search -- Invited Industrial Presentations -- Comparing Symbolic and Explicit Model Checking of a Software System -- Industrial Model Checking Based on Satisfiability Solvers -- A Typical Testing Problem: Validating WML Cellphones -- Model Checking Tools -- Heuristic Model Checking for Java Programs -- System Specification and Verification Using High Level Concepts ? A Tool Demonstration -- Demonstration of an Automated Integrated Test Environment for Web-Based Applications -- ?SPIN: Extending SPIN with Abstraction. 330 $aThe SPIN workshop series brings together researchers and practitioners interested in explicit state model checking technology as it is applied to the verification of software systems. Since 1995, when the SPIN workshop series was instigated, SPIN workshops have been held on an annual basis at Montre?al (1995), New Brunswick (1996), Enschede (1997), Paris (1998), Trento (1999), Toulouse (1999), Stanford (2000), and Toronto(2001). While the first SPIN workshop was a stand-alone event, later workshops have been organized as more or less closely affiliated events with larger conferences, in particular with CAV (1996), TACAS (1997), FORTE/PSTV (1998), FLOC (1999), World Congress on Formal Methods (1999), FMOODS (2000), and ICSE (2001). This year, SPIN 2002 was held as a satellite event of ETAPS 2002, the European Joint Conferences on Theory and Practice of Software. The co-location of SPIN workshops with conferences has proven to be very successful and has helped to disseminate SPIN model checking technology to wider audiences. Since 1999, the proceedings of the SPIN workshops have appeared in Springer-Verlag?s ?Lecture Notes in Computer Science? series. The history of successful SPIN workshops is evidence for the maturing of model checking technology, not only in the hardware domain, but increasingly also in the software area. While in earlier years algorithms and tool development 1 around the SPIN model checker were the focus of this workshop series, the scopehasrecentlywidenedtoincludemoregeneralapproachestosoftwaremodel checking. Current research in this area concentrates not so much on completely verifying system models, but rather on analyzing source code in order to discover software faults. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2318 606 $aComputer simulation 606 $aSoftware engineering 606 $aComputer logic 606 $aProgramming languages (Electronic computers) 606 $aSimulation and Modeling$3https://scigraph.springernature.com/ontologies/product-market-codes/I19000 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 615 0$aComputer simulation. 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aProgramming languages (Electronic computers) 615 14$aSimulation and Modeling. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aProgramming Languages, Compilers, Interpreters. 676 $a005.1/4 702 $aBosnacki$b Dragan$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aLeue$b Stefan$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational SPIN Workshop. 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143909703321 996 $aModel Checking Software$93359484 997 $aUNINA