國立虎尾科技大學 |

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 /

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Leveraging Applications of Formal Methods, Verification and Validation: Applications/ edited by Tiziana Margaria, Bernhard Steffen.
Reminder of title:	9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III /
other author:	Steffen, Bernhard.
Description:	XV, 490 p. 840 illus., 83 illus. in color.online resource. :
Contained By:	Springer Nature eBook
Subject:	Computer System Implementation. -
Online resource:	https://doi.org/10.1007/978-3-030-61467-6
ISBN:	9783030614676

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 /
Leveraging Applications of Formal Methods, Verification and Validation: Applications9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III /[electronic resource] :edited by Tiziana Margaria, Bernhard Steffen. - 1st ed. 2020. - XV, 490 p. 840 illus., 83 illus. in color.online resource. - Theoretical Computer Science and General Issues ;12478. - Theoretical Computer Science and General Issues ;9163.

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.

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

ISBN: 9783030614676

Standard No.: 10.1007/978-3-030-61467-6doiSubjects--Topical Terms:

669803
Computer System Implementation.

LC Class. No.: QA76.758

Dewey Class. No.: 005.1

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 /
LDR:05024nam a22004215i 4500 001 1018012
003 DE-He213
005 20201026054311.0
007 cr nn 008mamaa
008 210318s2020 gw | s |||| 0|eng d
020 $a 9783030614676 $9 978-3-030-61467-6
024 7 $a 10.1007/978-3-030-61467-6 $2 doi
035 $a 978-3-030-61467-6
050 4 $a QA76.758
072 7 $a UMZ $2 bicssc
072 7 $a COM051230 $2 bisacsh
072 7 $a UMZ $2 thema
072 7 $a UL $2 thema
082 0 4 $a 005.1 $2 23
245 1 0 $a Leveraging Applications of Formal Methods, Verification and Validation: Applications $h [electronic resource] : $b 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III / $c edited by Tiziana Margaria, Bernhard Steffen.
250 $a 1st ed. 2020.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2020.
300 $a XV, 490 p. 840 illus., 83 illus. in color. $b online resource.
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
347 $a text file $b PDF $2 rda
490 1 $a Theoretical Computer Science and General Issues ; $v 12478
505 0 $a 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.
520 $a 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. .
650 2 4 $a Computer System Implementation. $3 669803
650 2 4 $a Special Purpose and Application-Based Systems. $3 669833
650 2 4 $a Artificial Intelligence. $3 646849
650 2 4 $a Mathematical Logic and Formal Languages. $3 670059
650 1 4 $a Software Engineering/Programming and Operating Systems. $3 669780
650 0 $a Architecture, Computer. $3 1255731
650 0 $a Special purpose computers. $3 1204562
650 0 $a Artificial intelligence. $3 559380
650 0 $a Mathematical logic. $2 bicssc $3 810627
650 0 $a Software engineering. $3 562952
700 1 $a Steffen, Bernhard. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 883233
700 1 $a Margaria, Tiziana. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 882002
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783030614669
776 0 8 $i Printed edition: $z 9783030614683
830 0 $a Theoretical Computer Science and General Issues ; $v 9163 $3 1253524
856 4 0 $u https://doi.org/10.1007/978-3-030-61467-6
912 $a ZDB-2-SCS
912 $a ZDB-2-SXCS
912 $a ZDB-2-LNC
950 $a Computer Science (SpringerNature-11645)
950 $a Computer Science (R0) (SpringerNature-43710)