Skip to main content
  • Conference proceedings
  • © 2020

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

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 12476)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): ISoLA: International Symposium on Leveraging Applications of Formal Methods

Conference proceedings info: ISoLA 2020.

Buy it now

Buying options

eBook USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (32 papers)

  1. Front Matter

    Pages i-xxiii
  2. Modularity and (De-)Composition in Verification

    1. Front Matter

      Pages 1-1
    2. Who Carries the Burden of Modularity?

      • Dilian Gurov, Reiner Hähnle, Eduard Kamburjan
      Pages 3-21
    3. On Testing Message-Passing Components

      • Alex Coto, Roberto Guanciale, Emilio Tuosto
      Pages 22-38
    4. Composing Communicating Systems, Synchronously

      • Franco Barbanera, Ivan Lanese, Emilio Tuosto
      Pages 39-59
    5. Modular Verification of JML Contracts Using Bounded Model Checking

      • Bernhard Beckert, Michael Kirsten, Jonas Klamroth, Mattias Ulbrich
      Pages 60-80
    6. On Slicing Software Product Line Signatures

      • Ferruccio Damiani, Michael Lienhardt, Luca Paolini
      Pages 81-102
    7. Assumption-Commitment Types for Resource Management in Virtually Timed Ambients

      • Einar Broch Johnsen, Martin Steffen, Johanna Beate Stumpf
      Pages 103-121
    8. Abstraction and Genericity in Why3

      • Jean-Christophe Filliâtre, Andrei Paskevich
      Pages 122-142
    9. An Interface Theory for Program Verification

      • Dirk Beyer, Sudeep Kanav
      Pages 168-186Open Access
    10. Scaling Correctness-by-Construction

      • Alexander Knüppel, Tobias Runge, Ina Schaefer
      Pages 187-207
  3. X-by-Construction: Correctness Meets Probability

    1. Front Matter

      Pages 209-209
    2. X-by-Construction

      • Maurice H. ter Beek, Loek Cleophas, Axel Legay, Ina Schaefer, Bruce W. Watson
      Pages 211-215
    3. Correctness by Construction for Probabilistic Programs

      • Annabelle McIver, Carroll Morgan
      Pages 216-239
    4. Components in Probabilistic Systems: Suitable by Construction

      • Christel Baier, Clemens Dubslaff, Holger Hermanns, Michaela Klauck, Sascha Klüppelholz, Maximilian A. Köhl
      Pages 240-261
    5. Behavioral Specification Theories: An Algebraic Taxonomy

      • Uli Fahrenberg, Axel Legay
      Pages 262-274
    6. Approximating Euclidean by Imprecise Markov Decision Processes

      • Manfred Jaeger, Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen, Peter Gjøl Jensen
      Pages 275-289
    7. Shield Synthesis for Reinforcement Learning

      • Bettina Könighofer, Florian Lorber, Nils Jansen, Roderick Bloem
      Pages 290-306
    8. Inferring Performance from Code: A Review

      • Emilio Incerto, Annalisa Napolitano, Mirco Tribastone
      Pages 307-322

About this book

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.

 

 

Editors and Affiliations

  • Lero, Limerick, Ireland

    Tiziana Margaria

  • TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Bibliographic Information

Buy it now

Buying options

eBook USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access