Título :	9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III
Tipo de documento:	documento electrónico
Autores:	Margaria, Tiziana, ; Steffen, Bernhard,
Mención de edición:	1 ed.
Editorial:	[s.l.] : Springer
Fecha de publicación:	2020
Número de páginas:	XV, 490 p. 840 ilustraciones, 83 ilustraciones en color.
ISBN/ISSN/DL:	978-3-030-61467-6
Nota general:	Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Palabras clave:	Ingeniería de software  Teoría de las máquinas  Inteligencia artificial  Computadoras  Propósitos especiales  Sistemas informáticos  Lenguajes formales y teoría de los autómatas  Sistemas de propósito especial y basados ​​en aplicaciones  Implementación de sistema informático
Índice Dewey:	005.1 Programación (Computadoras)
Resumen:	El conjunto de tres volúmenes LNCS 12476 - 12478 constituye las actas arbitradas del 9.º Simposio internacional sobre el aprovechamiento de aplicaciones de métodos formales, ISoLA 2020, que estaba previsto que se llevara a cabo del 20 al 30 de octubre de 2020 en Rodas, Grecia. El evento en sí se pospuso hasta 2021 debido a la pandemia de COVID-19. Los artículos presentados fueron cuidadosamente revisados ​​y seleccionados para su inclusión en las actas. Cada volumen se centra en un tema individual con títulos de secciones temáticas dentro del volumen: Parte I, Principios de verificación: modularidad y (des)composición en la verificación; X por construcción: la corrección se encuentra con la probabilidad; 30 años de verificación de modelos estadísticos; Verificación y Validación de Sistemas Concurrentes y Distribuidos. Parte II, Principios de ingeniería: Automatización de la reingeniería del software; Ingeniería Rigurosa de Sistemas Adaptativos Colectivos. Parte III, Aplicaciones: Contratos inteligentes confiables: estado del arte, aplicaciones, desafíos y direcciones futuras; Verificación automatizada del software de control integrado; Métodos formales para la Computación Distribuida en futuros sistemas FERROVIARIOS. .
Nota de contenido:	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.
En línea:	https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
Link:	https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i

9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III [documento electrónico] / Margaria, Tiziana, ; Steffen, Bernhard,  . -  1 ed.  . - [s.l.] : Springer, 2020 . - XV, 490 p. 840 ilustraciones, 83 ilustraciones en color.
ISBN : 978-3-030-61467-6
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.

Palabras clave:	Ingeniería de software  Teoría de las máquinas  Inteligencia artificial  Computadoras  Propósitos especiales  Sistemas informáticos  Lenguajes formales y teoría de los autómatas  Sistemas de propósito especial y basados ​​en aplicaciones  Implementación de sistema informático
Índice Dewey:	005.1 Programación (Computadoras)
Resumen:	El conjunto de tres volúmenes LNCS 12476 - 12478 constituye las actas arbitradas del 9.º Simposio internacional sobre el aprovechamiento de aplicaciones de métodos formales, ISoLA 2020, que estaba previsto que se llevara a cabo del 20 al 30 de octubre de 2020 en Rodas, Grecia. El evento en sí se pospuso hasta 2021 debido a la pandemia de COVID-19. Los artículos presentados fueron cuidadosamente revisados ​​y seleccionados para su inclusión en las actas. Cada volumen se centra en un tema individual con títulos de secciones temáticas dentro del volumen: Parte I, Principios de verificación: modularidad y (des)composición en la verificación; X por construcción: la corrección se encuentra con la probabilidad; 30 años de verificación de modelos estadísticos; Verificación y Validación de Sistemas Concurrentes y Distribuidos. Parte II, Principios de ingeniería: Automatización de la reingeniería del software; Ingeniería Rigurosa de Sistemas Adaptativos Colectivos. Parte III, Aplicaciones: Contratos inteligentes confiables: estado del arte, aplicaciones, desafíos y direcciones futuras; Verificación automatizada del software de control integrado; Métodos formales para la Computación Distribuida en futuros sistemas FERROVIARIOS. .
Nota de contenido:	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.
En línea:	https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
Link:	https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i