𝔖 Scriptorium
✦   LIBER   ✦
📁

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

✍ Scribed by Tiziana Margaria, Bernhard Steffen

Publisher
Springer International Publishing;Springer
Year
2020
Tongue
English
Leaves
498
Series
Lecture Notes in Computer Science 12478
Edition
1st ed.
Category
Library
⬇  Acquire This Volume

No coin nor oath required. For personal study only.

✦ Synopsis

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.

✦ Table of Contents

Front Matter ....Pages i-xv
Front Matter ....Pages 1-1
Reliable Smart Contracts (Gordon J. Pace, César Sánchez, Gerardo Schneider)....Pages 3-8
Functional Verification of Smart Contracts via Strong Data Integrity (Wolfgang Ahrendt, Richard Bubel)....Pages 9-24
Bitcoin Covenants Unchained (Massimo Bartoletti, Stefano Lande, Roberto Zunino)....Pages 25-42
Specifying Framing Conditions for Smart Contracts (Bernhard Beckert, Jonas Schiffl)....Pages 43-59
Making Tezos Smart Contracts More Reliable with Coq (Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, Julien Tesson)....Pages 60-72
UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms (Lars Brünjes, Murdoch J. Gabbay)....Pages 73-88
Native Custom Tokens in the Extended UTXO Model (Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones et al.)....Pages 89-111
UTXO(_{\textsf {ma}}): UTXO with Multi-asset Support (Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones et al.)....Pages 112-130
Towards Configurable and Efficient Runtime Verification of Blockchain Based Smart Contracts at the Virtual Machine Level (Joshua Ellul)....Pages 131-145
Compiling Quantitative Type Theory to Michelson for Compile-Time Verification and Run-time Efficiency in Juvix (Christopher Goes)....Pages 146-160
Efficient Static Analysis of Marlowe Contracts (Pablo Lamela Seijas, David Smith, Simon Thompson)....Pages 161-177
Accurate Smart Contract Verification Through Direct Modelling (Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, Natasha Sharygina)....Pages 178-194
Smart Derivatives: On-Chain Forwards for Digital Assets (Alfonso D. D. M. Rius, Eamonn Gashier)....Pages 195-211
The Good, The Bad and The Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts (Clara Schneidewind, Markus Scherer, Matteo Maffei)....Pages 212-231
Front Matter ....Pages 233-233
Automated Verification of Embedded Control Software (Dilian Gurov, Paula Herber, Ina Schaefer)....Pages 235-239
A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System (Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Giuseppe Scaglione et al.)....Pages 240-254
Guess What I’m Doing! (Martin Fränzle, Paul Kröger)....Pages 255-272
On the Industrial Application of Critical Software Verification with VerCors (Marieke Huisman, Raúl E. Monti)....Pages 273-292
A Concept of Scenario Space Exploration with Criticality Coverage Guarantees (Hardi Hungar)....Pages 293-306
Towards Automated Service-Oriented Verification of Embedded Control Software Modeled in Simulink (Timm Liebrenz, Paula Herber, Sabine Glesner)....Pages 307-325
Verifying Safety Properties of Robotic Plans Operating in Real-World Environments via Logic-Based Environment Modeling (Tim Meywerk, Marcel Walter, Vladimir Herdt, Jan Kleinekathöfer, Daniel Große, Rolf Drechsler)....Pages 326-347
Formally Proving Compositionality in Industrial Systems with Informal Specifications (Mattias Nyberg, Jonas Westman, Dilian Gurov)....Pages 348-365
Specification, Synthesis and Validation of Strategies for Collaborative Embedded Systems (Bernd-Holger Schlingloff)....Pages 366-385
Front Matter ....Pages 387-387
Formal Methods for Distributed Computing in Future Railway Systems (Alessandro Fantechi, Stefania Gnesi, Anne E. Haxthausen)....Pages 389-392
Ensuring Safety with System Level Formal Modelling (Thierry Lecomte, Mathieu Comptier, Julien Molinero, Denis Sabatier)....Pages 393-403
A Modular Design Framework to Assess Intelligent Trains (Simon Collart-Dutilleul, Philippe Bon)....Pages 404-414
Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL (Per Lange Laursen, Van Anh Thi Trinh, Anne E. Haxthausen)....Pages 415-433
New Distribution Paradigms for Railway Interlocking (Jan Peleska)....Pages 434-448
Model Checking a Distributed Interlocking System Using k-induction with RT-Tester (Signe Geisler, Anne E. Haxthausen)....Pages 449-466
Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers (Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Laura Masullo et al.)....Pages 467-485
Back Matter ....Pages 487-490

✦ Subjects

Computer Science; Software Engineering/Programming and Operating Systems; Mathematical Logic and Formal Languages; Special Purpose and Application-Based Systems; Computer System Implementation

📜 SIMILAR VOLUMES

Leveraging Applications of Formal Method
📁 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
✍ Tiziana Margaria, Bernhard Steffen 📂 Library 📅 2020 🏛 Springer International Publishing;Springer 🌐 English

<p><p>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

Leveraging Applications of Formal Method
📁 Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II
✍ Tiziana Margaria, Bernhard Steffen 📂 Library 📅 2020 🏛 Springer International Publishing;Springer 🌐 English

<p><p>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

Leveraging Applications of Formal Method
📁 Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles: 11th International Symposium, ISoLA 2022 Rhodes, Greece, October 22–30, 2022 Proceedings, Part I
✍ Tiziana Margaria, Bernhard Steffen 📂 Library 📅 2022 🏛 Springer 🌐 English

<p><span>This 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. </span></p><p><span>The contributions in

Leveraging Applications of Formal Method
📁 Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part I
✍ Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Helmut Veith ( 📂 Library 📅 2010 🏛 Springer-Verlag Berlin Heidelberg 🌐 English

The two volume set LNCS 6415 and LNCS 6416 constitutes the refereed proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2010, held in Heraklion, Crete, Greece, in October 2010. The 100 revised full papers presented were carefully revised and selected fr

Leveraging Applications of Formal Method
📁 Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II
✍ Alessandro Moschitti (auth.), Tiziana Margaria, Bernhard Steffen (eds.) 📂 Library 📅 2010 🏛 Springer-Verlag Berlin Heidelberg 🌐 English

<p>The two volume set LNCS 6415 and LNCS 6416 constitutes the refereed proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2010, held in Heraklion, Crete, Greece, in October 2010. </p><p>The 100 revised full papers presented were carefully revised and s

Leveraging Applications of Formal Method
📁 Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II
✍ Tiziana Margaria, Bernhard Steffen 📂 Library 📅 2010 🏛 Springer 🌐 English

The two volume set LNCS 6415 and LNCS 6416 constitutes the refereed proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2010, held in Heraklion, Crete, Greece, in October 2010. The 100 revised full papers presented were carefully revised and selected