LEADER 03958nam  22007575  450 
001 9910494555103321
005 20230329224506.0
010   $a3-030-84629-6
024 7 $a10.1007/978-3-030-84629-9
035   $a(CKB)4100000011994672
035   $a(DE-He213)978-3-030-84629-9
035   $a(MiAaPQ)EBC6688988
035   $a(Au-PeEL)EBL6688988
035   $a(OCoLC)1263026170
035   $a(PPN)257350616
035   $a(EXLCZ)994100000011994672
100   $a20210802d2021      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 10$aModel Checking Software $e27th International Symposium, SPIN 2021, Virtual Event, July 12, 2021, Proceedings /$fedited by Alfons Laarman, Ana Sokolova
205   $a1st ed. 2021.
210  1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2021.
215   $a1 online resource (X, 195 p. 70 illus., 43 illus. in color.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12864
311   $a3-030-84628-8 
320   $aIncludes bibliographical references and index.
327   $aInvited Talks -- The marriage between safety and cybersecurity: still practicing -- A Hands-on Introduction to Spatial Model Checking using VoxLogicA -- Model Checking -- Accelerating the Computation of Dead and Concurrent Places using Reductions -- Spotlight Abstraction in Model Checking Real-Time Task Schedulability -- Verifying Pipeline Implementations in OpenMP -- Tool Papers -- C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs -- PatEC: Pattern-based Equivalence Checking -- Go2Pins: a framework for the LTL verification of Go programs -- Probabilistic Model Checking of Randomized Java Code -- Case Studies -- A model-checked I2C specification.
330   $aThis book constitutes the refereed proceedings of the 27th International Symposium on Model Checking Software, SPIN 2021, held virtually in July 2021. The 3 full papers, 4 tool papers, and 1 case study presented together with 2 invited talks were carefully reviewed and selected from 20 submissions. Topics covered include formal verification techniques for automated analysis of software; formal analysis for modeling languages, such as UML/state charts; formal specification languages, temporal logic, design-by-contract; model checking, automated theorem proving, including SAT and SMT; verifying compilers; abstraction and symbolic execution techniques; and much more.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12864
606   $aSoftware engineering
606   $aMachine theory
606   $aComputer science
606   $aAlgorithms
606   $aComputer simulation
606   $aComputers, Special purpose
606   $aSoftware Engineering
606   $aFormal Languages and Automata Theory
606   $aComputer Science Logic and Foundations of Programming
606   $aDesign and Analysis of Algorithms
606   $aComputer Modelling
606   $aSpecial Purpose and Application-Based Systems
615  0$aSoftware engineering.
615  0$aMachine theory.
615  0$aComputer science.
615  0$aAlgorithms.
615  0$aComputer simulation.
615  0$aComputers, Special purpose.
615 14$aSoftware Engineering.
615 24$aFormal Languages and Automata Theory.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aDesign and Analysis of Algorithms.
615 24$aComputer Modelling.
615 24$aSpecial Purpose and Application-Based Systems.
676   $a005.14
702   $aLaarman$b Alfons
702   $aSokolova$b Ana
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910494555103321
996   $aModel Checking Software$93359484
997   $aUNINA