Autor Steffen, Bernhard
|
|
Documentos disponibles escritos por este autor (14)
Hacer una sugerencia Refinar búsqueda10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / Margaria, Tiziana ; Steffen, Bernhard
Título : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings 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: 2021 Número de páginas: XII, 504 p. 124 ilustraciones, 71 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-89159-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 Inteligencia artificial Programación de computadoras Compiladores (programas informáticos) Software de la aplicacion Técnicas de programación Compiladores e intérpretes Aplicaciones informáticas y de sistemas de información Índice Dewey: 005.1 Programación (Computadoras) Resumen: Este libro constituye contribuciones de los eventos asociados a ISOLA 2021. En total, ISoLA 2021 comprende contribuciones de las actas originalmente previstas para ISoLA 2020 recopiladas en 4 volúmenes, LNCS 12476: Principios de verificación, LNCS 12477: Principios de ingeniería, LNCS 12478: Aplicaciones y LNCS 12479: Herramientas y tendencias. Las contribuciones incluidas en este volumen se organizaron en las siguientes secciones temáticas: 6ª Escuela Internacional de Ingeniería Rigurosa de Sistemas de Software basada en Herramientas; Pista Industrial; Programación: ¿Qué sigue? Herramientas de verificación de software; Ingeniería Rigurosa de Sistemas Adaptativos Colectivos. . Nota de contenido: STRESS - Introduction -- An Introduction to Graphical Modeling of CI/CD Workflows with Rig -- Pyrus: an Online Modeling Environment for No-Code Data-Analytics Service Composition -- Integrating External Services in DIME -- Asking Why -- Formal Methods for a Digital Industry: Industrial Day at ISoLA 2021 -- Agile Business Engineering: From Transformation Towards Continuous Innovation -- Towards Living Canvases -- Use Cases for Simulation in the Development of Automated Driving Systems -- Simulation-based Elicitation of Accuracy Requirements for the Environmental Perception of Autonomous Vehicles -- DSLs and Middleware Platforms in a Model-Driven Development Approach for Secure Predictive Maintenance Systems in Smart Factories -- From Requirements to Executable Rules: An Ensemble of Domain-Specific Languages for Programming Cyber-Physical Systems in Warehouse Logistics -- Mining Data Quality Rules for Data Migrations: A Case Study on Material Master Data -- Programming - What is Next? -- Low-Codeis Often High-Code, So We Must Design Low-Code Platforms to Enable Proper Software Engineering -- Time for All Programs, Not Just Real-Time Programs -- Integrated Modeling and Development of Component-Based Embedded Software in Scala -- Slang: The Sireum Programming Language -- HAMR: An AADL Multi-Platform Code Generation Toolset -- Fundamental Constructs in Programming Languages -- Introducing Dynamical Systems and Chaos Early in Computer Science and Software Engineering Education can Help Advance Theory and Practice of Software Development and Computing -- GATE: Gradual Effect Types -- Fixing Classification: A Viewpoint-based Approach -- The Future of Programming and Modelling: a Vision -- Towards Model-based Intent-Driven Adaptive Software -- The Interoperability Challenge: Building a model driven Digital Thread platform for CPS -- Programming vs. That Thing Subject Matter Experts Do -- Aligned, Purpose-Driven Cooperation: The Future Way of System Development -- RAILS: Roadmaps for AI integration in the raiL Sector -- A Journey through Software Model Checking of Interlocking Programs -- Supporting the Development of Hybrid ERTMS/ETCS Level 3 with Formal Modelling, Analysis and Simulation -- Formal Methods in Railway Signalling Infrastructure Standardisation Processes -- sVerify: Verifying Smart Contracts through Lazy Annotation and Learning -- Verifying temporal properties of stigmergic collective systems using CADP. 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 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings [documento electrónico] / Margaria, Tiziana, ; Steffen, Bernhard, . - 1 ed. . - [s.l.] : Springer, 2021 . - XII, 504 p. 124 ilustraciones, 71 ilustraciones en color.
ISBN : 978-3-030-89159-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 Inteligencia artificial Programación de computadoras Compiladores (programas informáticos) Software de la aplicacion Técnicas de programación Compiladores e intérpretes Aplicaciones informáticas y de sistemas de información Índice Dewey: 005.1 Programación (Computadoras) Resumen: Este libro constituye contribuciones de los eventos asociados a ISOLA 2021. En total, ISoLA 2021 comprende contribuciones de las actas originalmente previstas para ISoLA 2020 recopiladas en 4 volúmenes, LNCS 12476: Principios de verificación, LNCS 12477: Principios de ingeniería, LNCS 12478: Aplicaciones y LNCS 12479: Herramientas y tendencias. Las contribuciones incluidas en este volumen se organizaron en las siguientes secciones temáticas: 6ª Escuela Internacional de Ingeniería Rigurosa de Sistemas de Software basada en Herramientas; Pista Industrial; Programación: ¿Qué sigue? Herramientas de verificación de software; Ingeniería Rigurosa de Sistemas Adaptativos Colectivos. . Nota de contenido: STRESS - Introduction -- An Introduction to Graphical Modeling of CI/CD Workflows with Rig -- Pyrus: an Online Modeling Environment for No-Code Data-Analytics Service Composition -- Integrating External Services in DIME -- Asking Why -- Formal Methods for a Digital Industry: Industrial Day at ISoLA 2021 -- Agile Business Engineering: From Transformation Towards Continuous Innovation -- Towards Living Canvases -- Use Cases for Simulation in the Development of Automated Driving Systems -- Simulation-based Elicitation of Accuracy Requirements for the Environmental Perception of Autonomous Vehicles -- DSLs and Middleware Platforms in a Model-Driven Development Approach for Secure Predictive Maintenance Systems in Smart Factories -- From Requirements to Executable Rules: An Ensemble of Domain-Specific Languages for Programming Cyber-Physical Systems in Warehouse Logistics -- Mining Data Quality Rules for Data Migrations: A Case Study on Material Master Data -- Programming - What is Next? -- Low-Codeis Often High-Code, So We Must Design Low-Code Platforms to Enable Proper Software Engineering -- Time for All Programs, Not Just Real-Time Programs -- Integrated Modeling and Development of Component-Based Embedded Software in Scala -- Slang: The Sireum Programming Language -- HAMR: An AADL Multi-Platform Code Generation Toolset -- Fundamental Constructs in Programming Languages -- Introducing Dynamical Systems and Chaos Early in Computer Science and Software Engineering Education can Help Advance Theory and Practice of Software Development and Computing -- GATE: Gradual Effect Types -- Fixing Classification: A Viewpoint-based Approach -- The Future of Programming and Modelling: a Vision -- Towards Model-based Intent-Driven Adaptive Software -- The Interoperability Challenge: Building a model driven Digital Thread platform for CPS -- Programming vs. That Thing Subject Matter Experts Do -- Aligned, Purpose-Driven Cooperation: The Future Way of System Development -- RAILS: Roadmaps for AI integration in the raiL Sector -- A Journey through Software Model Checking of Interlocking Programs -- Supporting the Development of Hybrid ERTMS/ETCS Level 3 with Formal Modelling, Analysis and Simulation -- Formal Methods in Railway Signalling Infrastructure Standardisation Processes -- sVerify: Verifying Smart Contracts through Lazy Annotation and Learning -- Verifying temporal properties of stigmergic collective systems using CADP. 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
Título : 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III Tipo de documento: documento electrónico Autores: Beyer, Dirk, ; Huisman, Marieke, ; Kordon, Fabrice, ; Steffen, Bernhard, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2019 Número de páginas: XXVII, 258 p. 449 ilustraciones, 25 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-17502-3 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: Ciencias de la Computación Ingeniería de software Teoría de las máquinas Ordenadores Profesiones Computadoras digitales electrónicas Simulación por ordenador Lógica informática y fundamentos de la programación Lenguajes formales y teoría de los autómatas La profesión informática Rendimiento y evaluación del sistema Modelado por computadora Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. . Nota de contenido: TOOLympics 2019: An Overview of Competitions in Formal Methods -- Confluence Competion 2019 -- International Competition on Runtime Verification (CRV) -- The Model Checking Contest (2019) -- The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models -- The Rewrite Engines Competitions: A RECtrospective -- RERS 2019: Combining Synthesis with Real-World Models -- SL-COMP: Competition of Solvers for Separation Logic -- Automatic Verification of C and Java Programs: SV-COMP 2019 -- The Termination and Complexity Competition -- Competition on Software Testing (Test-Comp) -- VerifyThis - Verification Competition with a Human Factor -- SV-COMP 2019 -- CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker (Competition Contribution) -- Extending DIVINE with Symbolic Verification using SMT (Competition Contribution) -- ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution) -- JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution) -- JayHorn: A Java Model Checker (Competition Contribution) -- Java Pathfinder at SV-COMP 2019 -- Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution) -- PeSCo: Predicting Sequential Combinations of Verifiers (Competition Contribution) -- Symbolic Pathfinder for SV-COMP -- VeriFuzz: Program Aware Fuzzing -- VIAP 1.1 (Competition Contribution). 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 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III [documento electrónico] / Beyer, Dirk, ; Huisman, Marieke, ; Kordon, Fabrice, ; Steffen, Bernhard, . - 1 ed. . - [s.l.] : Springer, 2019 . - XXVII, 258 p. 449 ilustraciones, 25 ilustraciones en color.
ISBN : 978-3-030-17502-3
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Palabras clave: Ciencias de la Computación Ingeniería de software Teoría de las máquinas Ordenadores Profesiones Computadoras digitales electrónicas Simulación por ordenador Lógica informática y fundamentos de la programación Lenguajes formales y teoría de los autómatas La profesión informática Rendimiento y evaluación del sistema Modelado por computadora Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. . Nota de contenido: TOOLympics 2019: An Overview of Competitions in Formal Methods -- Confluence Competion 2019 -- International Competition on Runtime Verification (CRV) -- The Model Checking Contest (2019) -- The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models -- The Rewrite Engines Competitions: A RECtrospective -- RERS 2019: Combining Synthesis with Real-World Models -- SL-COMP: Competition of Solvers for Separation Logic -- Automatic Verification of C and Java Programs: SV-COMP 2019 -- The Termination and Complexity Competition -- Competition on Software Testing (Test-Comp) -- VerifyThis - Verification Competition with a Human Factor -- SV-COMP 2019 -- CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker (Competition Contribution) -- Extending DIVINE with Symbolic Verification using SMT (Competition Contribution) -- ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution) -- JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution) -- JayHorn: A Java Model Checker (Competition Contribution) -- Java Pathfinder at SV-COMP 2019 -- Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution) -- PeSCo: Predicting Sequential Combinations of Verifiers (Competition Contribution) -- Symbolic Pathfinder for SV-COMP -- VeriFuzz: Program Aware Fuzzing -- VIAP 1.1 (Competition Contribution). 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
Título : 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I 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: XXIII, 582 p. 2427 ilustraciones, 110 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-61362-4 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 Ciencias de la Computación Inteligencia artificial Sistemas informáticos Lógica informática y fundamentos de la programación 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: Who Carries the Burden of Modularity? -- On Testing Message-Passing Components -- Composing Communicating Systems, Synchronously -- Modular Verification of JML Contracts Using Bounded Model Checking -- On Slicing Software Product Line Signatures -- Assumption-Commitment Types for Resource Management in Virtually Timed Ambients -- Abstraction and Genericity in Why3 -- Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework -- An Interface Theory for Program Verification -- Scaling Correctness-by-Construction -- X-by-Construction: Correctness meets Probability -- Correctness by construction for probabilistic programs -- Components in Probabilistic Systems: Suitable by Construction -- Behavioral Specification Theories: an Algebraic Taxonomy -- Approximating Euclidean by Imprecise Markov Decision Processes -- Shield Synthesis for Reinforcement Learning -- Inferring Performance From Code: A Review -- 30 years of Statistical Model Checking -- Statistical Model Checking: Black or White? -- Probabilistic Mission Planning and Analysis for Multi-agent Systems -- 30 Years of Simulation-Based Quantitative Analysis Tools: a Comparison Experiment between Möbius and Uppaal SMC -- Fluid Model-Checking in UPPAAL for Covid-19 -- Improving Secure and Robust Patient Service Delivery -- Verification and Validation of Concurrent and Distributed Systems (Track Summary) -- Step-wise Development of Provably Correct Actor Systems -- Violation Witnesses and Result Validation for Multi-Threaded Programs -- Tendermint Blockchain Synchronization: Formal Specification and Model Checking -- Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project -- Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs -- Formal Verification of an Industrial Distributed Algorithm: an Experience Report -- Deploying TESTAR to enable remote testing in an industrial CI pipeline: a case-based evaluation -- A Formal Model of the Kubernetes Container Framework. 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 I [documento electrónico] / Margaria, Tiziana, ; Steffen, Bernhard, . - 1 ed. . - [s.l.] : Springer, 2020 . - XXIII, 582 p. 2427 ilustraciones, 110 ilustraciones en color.
ISBN : 978-3-030-61362-4
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 Ciencias de la Computación Inteligencia artificial Sistemas informáticos Lógica informática y fundamentos de la programación 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: Who Carries the Burden of Modularity? -- On Testing Message-Passing Components -- Composing Communicating Systems, Synchronously -- Modular Verification of JML Contracts Using Bounded Model Checking -- On Slicing Software Product Line Signatures -- Assumption-Commitment Types for Resource Management in Virtually Timed Ambients -- Abstraction and Genericity in Why3 -- Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework -- An Interface Theory for Program Verification -- Scaling Correctness-by-Construction -- X-by-Construction: Correctness meets Probability -- Correctness by construction for probabilistic programs -- Components in Probabilistic Systems: Suitable by Construction -- Behavioral Specification Theories: an Algebraic Taxonomy -- Approximating Euclidean by Imprecise Markov Decision Processes -- Shield Synthesis for Reinforcement Learning -- Inferring Performance From Code: A Review -- 30 years of Statistical Model Checking -- Statistical Model Checking: Black or White? -- Probabilistic Mission Planning and Analysis for Multi-agent Systems -- 30 Years of Simulation-Based Quantitative Analysis Tools: a Comparison Experiment between Möbius and Uppaal SMC -- Fluid Model-Checking in UPPAAL for Covid-19 -- Improving Secure and Robust Patient Service Delivery -- Verification and Validation of Concurrent and Distributed Systems (Track Summary) -- Step-wise Development of Provably Correct Actor Systems -- Violation Witnesses and Result Validation for Multi-Threaded Programs -- Tendermint Blockchain Synchronization: Formal Specification and Model Checking -- Safe Sessions of Channel Actions in Clojure: A Tour of the Discourje Project -- Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs -- Formal Verification of an Industrial Distributed Algorithm: an Experience Report -- Deploying TESTAR to enable remote testing in an industrial CI pipeline: a case-based evaluation -- A Formal Model of the Kubernetes Container Framework. 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
Título : 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II 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, 544 p. 791 ilustraciones, 658 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-61470-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 Ciencias de la Computación Inteligencia artificial Sistemas informáticos Lógica informática y fundamentos de la programación 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: Automating Software Re-Engineering (Introduction to the ISoLA 2020 Track) -- Formal Verification of Developer Tests: a Research Agenda Inspired by Mutation Testing -- Modular Regression Verification for Reactive Systems -- Finding Idioms in Source Code using Subtree Counting Techniques -- Parametric Timed Bisimulation -- A Unifying Framework for Dynamic Monitoring and a Taxonomy of Optimizations -- Thirty-seven years of relational Hoare logic: remarks on its principles and history -- Safer Parallelization -- Refactoring and Active Object Languages -- Rigorous Engineering of Collective Adaptive Systems -- Introduction to the 3rd Track Edition -- Composition of Component Models - a Key to Construct Big Systems -- Degrees of Autonomy in Coordinating Collectives of Self-Driving Vehicles -- Engineering semantic self-composition of services through tuple-based coordination -- A Dynamic Logic for Systems with Predicate-based Communication -- Behavioural Abstractions for Collective AdaptiveSystems -- Verifying AbC specifications via emulation -- Adaptive Security Policies -- Capturing Dynamicity and Uncertainty in Security and Trust via Situational Patterns -- Guaranteeing Type Consistency in Collective Adaptive Systems -- Epistemic Logic in Ensemble Specification -- FScaFi: a Core Calculus for Collective Adaptive Systems Programming -- Writing Robotics Applications with X-Klaim -- Measuring Adaptability and Reliability of Large Scaled Systems -- Centrality-preserving exact reductions of Multi-Layer Networks -- Towards Dynamic Dependable Systems through Evidence-Based Continuous Certification -- Forming Ensembles at Runtime: A Machine Learning Approach -- Synthesizing Control for a System with Black Box Environment, based on Deep Learning -- A Formal Model For Reasoning About The Ideal Fitness In Evolutionary Processes -- A case study of policy synthesis for swarm robotics. -- Maple-Swarm: Programming Collective Behavior for Ensembles by extending HTN-Planning -- Swarm and Collective Capabilities for Multipotent Robot Ensembles. 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 II [documento electrónico] / Margaria, Tiziana, ; Steffen, Bernhard, . - 1 ed. . - [s.l.] : Springer, 2020 . - XV, 544 p. 791 ilustraciones, 658 ilustraciones en color.
ISBN : 978-3-030-61470-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 Ciencias de la Computación Inteligencia artificial Sistemas informáticos Lógica informática y fundamentos de la programación 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: Automating Software Re-Engineering (Introduction to the ISoLA 2020 Track) -- Formal Verification of Developer Tests: a Research Agenda Inspired by Mutation Testing -- Modular Regression Verification for Reactive Systems -- Finding Idioms in Source Code using Subtree Counting Techniques -- Parametric Timed Bisimulation -- A Unifying Framework for Dynamic Monitoring and a Taxonomy of Optimizations -- Thirty-seven years of relational Hoare logic: remarks on its principles and history -- Safer Parallelization -- Refactoring and Active Object Languages -- Rigorous Engineering of Collective Adaptive Systems -- Introduction to the 3rd Track Edition -- Composition of Component Models - a Key to Construct Big Systems -- Degrees of Autonomy in Coordinating Collectives of Self-Driving Vehicles -- Engineering semantic self-composition of services through tuple-based coordination -- A Dynamic Logic for Systems with Predicate-based Communication -- Behavioural Abstractions for Collective AdaptiveSystems -- Verifying AbC specifications via emulation -- Adaptive Security Policies -- Capturing Dynamicity and Uncertainty in Security and Trust via Situational Patterns -- Guaranteeing Type Consistency in Collective Adaptive Systems -- Epistemic Logic in Ensemble Specification -- FScaFi: a Core Calculus for Collective Adaptive Systems Programming -- Writing Robotics Applications with X-Klaim -- Measuring Adaptability and Reliability of Large Scaled Systems -- Centrality-preserving exact reductions of Multi-Layer Networks -- Towards Dynamic Dependable Systems through Evidence-Based Continuous Certification -- Forming Ensembles at Runtime: A Machine Learning Approach -- Synthesizing Control for a System with Black Box Environment, based on Deep Learning -- A Formal Model For Reasoning About The Ideal Fitness In Evolutionary Processes -- A case study of policy synthesis for swarm robotics. -- Maple-Swarm: Programming Collective Behavior for Ensembles by extending HTN-Planning -- Swarm and Collective Capabilities for Multipotent Robot Ensembles. 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
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
PermalinkPermalink
Permalink
Permalink
Permalink
PermalinkPermalinkPermalink
Permalink
