LEADER 04057nam  22007335  450 
001 9910483304503321
005 20230222192415.0
010   $a3-319-17404-5
024 7 $a10.1007/978-3-319-17404-4
035   $a(CKB)3710000000404067
035   $a(SSID)ssj0001501746
035   $a(PQKBManifestationID)11918423
035   $a(PQKBTitleCode)TC0001501746
035   $a(PQKBWorkID)11446656
035   $a(PQKB)10609962
035   $a(DE-He213)978-3-319-17404-4
035   $a(MiAaPQ)EBC6303222
035   $a(MiAaPQ)EBC5577023
035   $a(Au-PeEL)EBL5577023
035   $a(OCoLC)908102372
035   $a(PPN)185489095
035   $a(EXLCZ)993710000000404067
100   $a20150416d2015      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aStructured Object-Oriented Formal Language and Method $e4th International Workshop, SOFL+MSVL 2014, Luxembourg, Luxembourg, November 6, 2014, Revised Selected Papers /$fedited by Shaoying Liu, Zhenhua Duan
205   $a1st ed. 2015.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2015.
215   $a1 online resource (VIII, 189 p. 74 illus.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8979
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-319-17403-7 
327   $aTesting and Inspection -- An Implementation Framework for Optimizing Test Case Generation Using Model Checking -- Applying GA with Tabu list for Automatically Generating Test Cases Based on Formal Specification -- Development of a Software Tool to Support Traceability-Based Inspection of SOFL Specifications -- Model Checking and Animation -- Unified Bounded Model Checking for MSVL -- An Over-Approximation Forward Analysis for Nested Timed Automata -- Adopting Variable Dependency in Animation for Presenting the Behaviour of Process -- Education and Verification -- Using Alloy in Introductory Courses of Formal Methods -- Automatic Verification for Later-Correspondence of Security Protocols -- Combining Separation Logic and Projection Temporal Logic to Reason About Non-blocking Concurrency -- Semantics and Analysis Formal Semantics of Orc Based on TLAž -- Incremental Points-to Analysis for Java via Edit Propagation -- A Memory Management Mechanism for MSVL.
330   $aThis book constitutes the thoroughly refereed post-workshop proceedings of the 4th International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2014, held in Luxembourg, Luxembourg, in November 2014. The 12 papers presented in this volume were carefully reviewed and selected from 20 submissions. They are organized in topical sections on testing and inspection; model checking and animation; education and verification; and semantics and analysis.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v8979
606   $aComputer science
606   $aSoftware engineering
606   $aCompilers (Computer programs)
606   $aMachine theory
606   $aComputer Science Logic and Foundations of Programming
606   $aSoftware Engineering
606   $aCompilers and Interpreters
606   $aFormal Languages and Automata Theory
615  0$aComputer science.
615  0$aSoftware engineering.
615  0$aCompilers (Computer programs).
615  0$aMachine theory.
615 14$aComputer Science Logic and Foundations of Programming.
615 24$aSoftware Engineering.
615 24$aCompilers and Interpreters.
615 24$aFormal Languages and Automata Theory.
676   $a004.0151
702   $aLiu$b Shaoying$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aDuan$b Zhenhua$4edt$4http://id.loc.gov/vocabulary/relators/edt
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483304503321
996   $aStructured Object-Oriented Formal Language and Method$93084063
997   $aUNINA