| Description |
1 online resource (xv, 490 pages) : illustrations (some color) |
| Series |
Lecture notes in computer science ; 12478 |
|
LNCS sublibrary, SL 1, Theoretical Computer Science and General Issues |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues ; 12478.
|
|
Lecture notes in computer science ; 12478.
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
Reliable Smart Contracts -- Track Introduction -- Functional Verification of Smart Contracts via Strong Data Integrity -- Bitcoin covenants unchained -- Specifying Framing Conditions for Smart Contracts -- Making Tezos smart contracts more reliable with Coq -- UTxO- vs account-based smart contract blockchain programming paradigms -- Native Custom Tokens in the Extended UTXO Model -- UTXOma: UTXO with Multi-Asset Support -- Towards Configurable and Efficient Runtime Verification of Blockchain based Smart Contracts at the Virtual Machine Level -- Compiling Quantitative Type Theory to Michelson for Compile-Time Verification & Run-time Efficiency in Juvix -- Efficient static analysis of Marlowe contracts -- Accurate Smart Contract Verification through Direct Modelling -- Smart Derivatives: On-chain Forwards for Digital Assets -- The Good, the Bad and the Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts -- Automated Verification of Embedded Control Software -- Track Introduction -- Model-Based Design, Verification and Deployment of Railway Interlocking System -- Guess What I'm Doing! Rendering Formal Verification Methods Ripe for the Era of Interacting Intelligent Systems -- On the Industrial Application of Critical Software Verification with VerCors -- A Concept of Scenario Space Exploration with Criticality Coverage Guarantees -- Towards Automated Service-oriented Verification of Embedded Control Software modeled in Simulink -- Verifying Safety Properties of Robotic Plans Operating in Real-World Environments via Logic-based Environment Modeling -- Formally Proving Compositionality in Industrial Systems with Informal Specifications -- Specification, Synthesis and Validation of Strategies for Collaborative Embedded Systems -- Formal methods for Distributed Computing in future Railway systems -- Ensuring Safety with System Level Formal Modelling -- A modular design framework to assess intelligent trains -- Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL -- New Distribution Paradigms for Railway Interlocking -- Model Checking a Distributed Interlocking System Using k-induction with RT-Tester -- Designing a Demonstrator of Formal Methods for Railways Infrastructure Managers |
| Summary |
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 |
| Notes |
International conference proceedings |
|
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed January 20, 2021) |
| Subject |
Formal methods (Computer science) -- Congresses
|
|
Computer software -- Verification -- Congresses
|
|
Software engineering -- Congresses
|
|
Software engineering.
|
|
Logic, Symbolic and mathematical.
|
|
Artificial intelligence.
|
|
Computers, Special purpose.
|
|
Computer architecture.
|
|
Artificial Intelligence
|
|
artificial intelligence.
|
|
Formal methods (Computer science)
|
|
Computer software -- Verification
|
|
Artificial intelligence
|
|
Computer architecture
|
|
Computers, Special purpose
|
|
Logic, Symbolic and mathematical
|
|
Software engineering
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Margaria-Steffen, Tiziana, 1964- editor
|
|
Steffen, Bernhard, editor
|
| ISBN |
9783030614676 |
|
3030614670 |
|
