000946860 000__ 06124cam\a2200649Ii\4500 000946860 001__ 946860 000946860 005__ 20230306152456.0 000946860 006__ m\\\\\o\\d\\\\\\\\ 000946860 007__ cr\nn\nnnunnun 000946860 008__ 201026s2020\\\\sz\a\\\\o\\\\\101\0\eng\d 000946860 019__ $$a1225934730 000946860 020__ $$a9783030614676$$q(electronic book) 000946860 020__ $$a3030614670$$q(electronic book) 000946860 020__ $$z9783030614669 000946860 0247_ $$a10.1007/978-3-030-61467-6$$2doi 000946860 035__ $$aSP(OCoLC)on1225892969 000946860 035__ $$aSP(OCoLC)1225892969$$z(OCoLC)1225934730 000946860 040__ $$aDCT$$beng$$cDCT$$dOCLCO$$dOCLCF$$dGW5XE$$dOCLCO$$dUPM$$dBDX 000946860 049__ $$aISEA 000946860 050_4 $$aQA76.9.F67$$bI83 2020eb 000946860 08204 $$a005.1$$223 000946860 1112_ $$aISoLA (Symposium)$$n(9th :$$d2020 :$$cOnline) 000946860 24510 $$aLeveraging applications of formal methods, verification and validation :$$bApplications : 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings.$$nPart III /$$cTiziana Margaria, Bernhard Steffen (eds.). 000946860 2463_ $$aISoLA 2020 000946860 2463_ $$aApplications 000946860 264_1 $$aCham :$$bSpringer,$$c2020. 000946860 300__ $$a1 online resource (xv, 490 pages) :$$bill. (some col.). 000946860 336__ $$atext$$btxt$$2rdacontent 000946860 337__ $$acomputer$$bc$$2rdamedia 000946860 338__ $$aonline resource$$bcr$$2rdacarrier 000946860 347__ $$atext file$$bPDF$$2rda 000946860 4901_ $$aLecture notes in computer science ;$$v12478 000946860 4901_ $$aLNCS sublibrary, SL 1, Theoretical Computer Science and General Issues 000946860 500__ $$aInternational conference proceedings. 000946860 500__ $$aIncludes author index. 000946860 5050_ $$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. 000946860 506__ $$aAccess limited to authorized users. 000946860 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. 000946860 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed January 20, 2021). 000946860 650_0 $$aFormal methods (Computer science)$$vCongresses. 000946860 650_0 $$aComputer software$$xVerification$$vCongresses. 000946860 650_0 $$aSoftware engineering$$vCongresses. 000946860 650_0 $$aSoftware engineering. 000946860 650_0 $$aLogic, Symbolic and mathematical. 000946860 650_0 $$aArtificial intelligence. 000946860 650_0 $$aComputers, Special purpose. 000946860 650_0 $$aComputer architecture. 000946860 7001_ $$aMargaria-Steffen, Tiziana,$$d1964-$$eeditor. 000946860 7001_ $$aSteffen, Bernhard,$$eeditor. 000946860 77608 $$iPrint version:$$z9783030614669 000946860 830_0 $$aLNCS sublibrary.$$nSL 1,$$pTheoretical computer science and general issues ;$$v12478. 000946860 830_0 $$aLecture notes in computer science ;$$v12478. 000946860 830_0 $$aLNCS sublibrary.$$nSL 1,$$pTheoretical computer science and general issues. 000946860 852__ $$bebk 000946860 85640 $$3SpringerLink$$uhttps://univsouthin.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-030-61467-6$$zOnline Access$$91397441.1 000946860 909CO $$ooai:library.usi.edu:946860$$pGLOBAL_SET 000946860 980__ $$aEBOOK 000946860 980__ $$aBIB 000946860 982__ $$aEbook 000946860 983__ $$aOnline 000946860 994__ $$a92$$bISE