Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I

The three-volume set LNCS 12476 - 12478 constitutes the refereed proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, which was planned to take place during October 20–30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the C...

Full description

Bibliographic Details
Other Authors: Margaria, Tiziana (Editor), Steffen, Bernhard (Editor)
Format: eBook
Language:English
Published: Cham Springer International Publishing 2020, 2020
Edition:1st ed. 2020
Series:Theoretical Computer Science and General Issues
Subjects:
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
LEADER 04657nmm a2200385 u 4500
001 EB001904023
003 EBX01000000000000001066929
005 00000000000000.0
007 cr|||||||||||||||||||||
008 201103 ||| eng
020 |a 9783030613624 
100 1 |a Margaria, Tiziana  |e [editor] 
245 0 0 |a Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles  |h Elektronische Ressource  |b 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I  |c edited by Tiziana Margaria, Bernhard Steffen 
250 |a 1st ed. 2020 
260 |a Cham  |b Springer International Publishing  |c 2020, 2020 
300 |a XXIII, 582 p. 2427 illus., 110 illus. in color  |b online resource 
505 0 |a Statistical Model Checking: Black or White? -- Probabilistic Mission Planning and Analysis for Multi-agent Systems -- 30 Years of Simulation-Based Quantitative Analysis Tools: a Comparison Experiment between Möbius and Uppaal SMC -- Fluid Model-Checking in UPPAAL for Covid-19 -- Improving Secure and Robust Patient Service Delivery -- Verification and Validation of Concurrent and Distributed Systems (Track Summary) -- Step-wise Development of Provably Correct Actor Systems -- Violation Witnesses and Result Validation for Multi-Threaded Programs -- Tendermint Blockchain Synchronization: Formal Specification and Model Checking -- Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project -- Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs -- Formal Verification of an Industrial Distributed Algorithm: an Experience Report -- Deploying TESTAR to enable remote testing in an industrial CI pipeline: a case-based evaluation --  
505 0 |a A Formal Model of the Kubernetes Container Framework 
505 0 |a Who Carries the Burden of Modularity? -- On Testing Message-Passing Components -- Composing Communicating Systems, Synchronously -- Modular Verification of JML Contracts Using Bounded Model Checking -- On Slicing Software Product Line Signatures -- Assumption-Commitment Types for Resource Management in Virtually Timed Ambients -- Abstraction and Genericity in Why3 -- Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework -- An Interface Theory for Program Verification -- Scaling Correctness-by-Construction -- X-by-Construction: Correctness meets Probability -- Correctness by construction for probabilistic programs -- Components in Probabilistic Systems: Suitable by Construction -- Behavioral Specification Theories: an Algebraic Taxonomy -- Approximating Euclidean by Imprecise Markov Decision Processes -- Shield Synthesis for Reinforcement Learning -- Inferring Performance From Code: A Review -- 30 years of Statistical Model Checking --  
653 |a Computer systems 
653 |a Computer Science Logic and Foundations of Programming 
653 |a Software engineering 
653 |a Computer science 
653 |a Computer System Implementation 
653 |a Artificial Intelligence 
653 |a Software Engineering 
653 |a Artificial intelligence 
700 1 |a Steffen, Bernhard  |e [editor] 
041 0 7 |a eng  |2 ISO 639-2 
989 |b Springer  |a Springer eBooks 2005- 
490 0 |a Theoretical Computer Science and General Issues 
028 5 0 |a 10.1007/978-3-030-61362-4 
856 4 0 |u https://doi.org/10.1007/978-3-030-61362-4?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 005.1 
520 |a The three-volume set LNCS 12476 - 12478 constitutes the refereed proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, which was planned to take place during October 20–30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the COVID-19 pandemic. The papers presented were carefully reviewed and selected for inclusion in the proceedings. Each volume focusses on an individual topic with topical section headings within the volume: Part I, Verification Principles: Modularity and (De-)Composition in Verification; X-by-Construction: Correctness meets Probability; 30 Years of Statistical Model Checking; Verification and Validation of Concurrent and Distributed Systems. Part II, Engineering Principles: Automating Software Re-Engineering; Rigorous Engineering of Collective Adaptive Systems. Part III, Applications: Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions; Automated Verification of Embedded Control Software; Formal methods for DIStributed COmputing in future RAILway systems.