000 05839nam a22006015i 4500
001 978-3-030-61467-6
003 DE-He213
005 20240423125048.0
007 cr nn 008mamaa
008 201026s2020 sz | s |||| 0|eng d
020 _a9783030614676
_9978-3-030-61467-6
024 7 _a10.1007/978-3-030-61467-6
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
072 7 _aUMZ
_2thema
082 0 4 _a005.1
_223
245 1 0 _aLeveraging Applications of Formal Methods, Verification and Validation: Applications
_h[electronic resource] :
_b9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III /
_cedited by Tiziana Margaria, Bernhard Steffen.
250 _a1st ed. 2020.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2020.
300 _aXV, 490 p. 840 illus., 83 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v12478
505 0 _aReliable 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.
520 _aThe 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. .
650 0 _aSoftware engineering.
650 0 _aMachine theory.
650 0 _aArtificial intelligence.
650 0 _aComputers, Special purpose.
650 0 _aComputer systems.
650 1 4 _aSoftware Engineering.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aArtificial Intelligence.
650 2 4 _aSpecial Purpose and Application-Based Systems.
650 2 4 _aComputer System Implementation.
700 1 _aMargaria, Tiziana.
_eeditor.
_0(orcid)
_10000-0002-5547-9739
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aSteffen, Bernhard.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783030614669
776 0 8 _iPrinted edition:
_z9783030614683
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v12478
856 4 0 _uhttps://doi.org/10.1007/978-3-030-61467-6
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c173798
_d173798