001450568 000__ 06240cam\a2200649\i\4500
001450568 001__ 1450568
001450568 003__ OCoLC
001450568 005__ 20230310004532.0
001450568 006__ m\\\\\o\\d\\\\\\\\
001450568 007__ cr\cn\nnnunnun
001450568 008__ 221023s2022\\\\sz\a\\\\o\\\\\101\0\eng\d
001450568 019__ $$a1348482928
001450568 020__ $$a9783031198496$$q(electronic bk.)
001450568 020__ $$a3031198492$$q(electronic bk.)
001450568 020__ $$z9783031198489
001450568 020__ $$z3031198484
001450568 0247_ $$a10.1007/978-3-031-19849-6$$2doi
001450568 035__ $$aSP(OCoLC)1348479080
001450568 040__ $$aYDX$$beng$$erda$$epn$$cYDX$$dGW5XE$$dEBLCP$$dOCLCF$$dOCLCQ
001450568 049__ $$aISEA
001450568 050_4 $$aQA76.9.F67$$bI83 2022
001450568 08204 $$a005.1$$223/eng/20221101
001450568 1112_ $$aISoLA (Symposium)$$n(11th :$$d2022 :$$cRhodes, Greece)
001450568 24510 $$aLeveraging applications of formal methods, verification and validation :$$bverification principles : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings.$$nPart I /$$cTiziana Margaria, Bernhard Steffen (eds.).
001450568 24630 $$aISoLA 2022
001450568 264_1 $$aCham :$$bSpringer,$$c[2022]
001450568 264_4 $$c©2022
001450568 300__ $$a1 online resource (xiii, 598 pages) :$$billustrations (some color).
001450568 336__ $$atext$$btxt$$2rdacontent
001450568 337__ $$acomputer$$bc$$2rdamedia
001450568 338__ $$aonline resource$$bcr$$2rdacarrier
001450568 4901_ $$aLecture notes in computer science ;$$v13701
001450568 500__ $$aInternational conference proceedings.
001450568 500__ $$aIncludes author index.
001450568 5050_ $$aIntro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis -- Bridging Gaps Between Program Specification Paradigms -- SpecifyThis -- Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory
001450568 5058_ $$a5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT
001450568 5058_ $$a4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge
001450568 5058_ $$a5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References -- Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References
001450568 5058_ $$aSpecification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References
001450568 506__ $$aAccess limited to authorized users.
001450568 520__ $$aThis four-volume set LNCS 13701-13704 constitutes contributions of the associated events held at the 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022, which took place in Rhodes, Greece, in October/November 2022. The contributions in the four-volume set are organized according to the following topical sections: specify this - bridging gaps between program specification paradigms; x-by-construction meets runtime verification; verification and validation of concurrent and distributed heterogeneous systems; programming - what is next: the role of documentation; automated software re-engineering; DIME day; rigorous engineering of collective adaptive systems; formal methods meet machine learning; digital twin engineering; digital thread in smart manufacturing; formal methods for distributed computing in future railway systems; industrial day.
001450568 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed November 1, 2022).
001450568 650_0 $$aFormal methods (Computer science)$$vCongresses.
001450568 650_0 $$aComputer software$$xVerification$$vCongresses.
001450568 650_0 $$aSoftware engineering$$vCongresses.
001450568 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772
001450568 655_0 $$aElectronic books.
001450568 7001_ $$aMargaria-Steffen, Tiziana,$$d1964-$$eeditor.
001450568 7001_ $$aSteffen, Bernhard,$$eeditor.
001450568 77608 $$iPrint version: $$z3031198484$$z9783031198489$$w(OCoLC)1346213854
001450568 830_0 $$aLecture notes in computer science ;$$v13701.
001450568 852__ $$bebk
001450568 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-031-19849-6$$zOnline Access$$91397441.1
001450568 909CO $$ooai:library.usi.edu:1450568$$pGLOBAL_SET
001450568 980__ $$aBIB
001450568 980__ $$aEBOOK
001450568 982__ $$aEbook
001450568 983__ $$aOnline
001450568 994__ $$a92$$bISE