| Título : |
13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings |
| Tipo de documento: |
documento electrónico |
| Autores: |
Dutle, Aaron, ; Moscato, Mariano M., ; Titolo, Laura, ; Muñoz, César A., ; Perez, Ivan, |
| Mención de edición: |
1 ed. |
| Editorial: |
[s.l.] : Springer |
| Fecha de publicación: |
2021 |
| Número de páginas: |
XVI, 402 p. 133 ilustraciones, 80 ilustraciones en color. |
| ISBN/ISSN/DL: |
978-3-030-76384-8 |
| 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 Ingeniería Informática Red de computadoras Inteligencia artificial Simulación por ordenador Teoría de la Computación Ingeniería Informática y Redes Modelado por computadora |
| Índice Dewey: |
005.1 Programación (Computadoras) |
| Resumen: |
Este libro constituye las actas del 13.º Simposio Internacional sobre Métodos Formales de la NASA, NFM 2021, celebrado virtualmente en mayo de 2021. Los 21 artículos completos y 3 breves presentados en este volumen fueron cuidadosamente revisados y seleccionados entre 66 presentaciones. Los documentos tienen como objetivo identificar desafíos y proporcionar soluciones para lograr garantía en sistemas de misión crítica y seguridad crítica. Ejemplos de tales sistemas incluyen algoritmos avanzados de garantía de separación para aeronaves, transporte aéreo de próxima generación, encuentro y acoplamiento autónomo de naves espaciales, software a bordo para sistemas aéreos no tripulados (UAS), gestión del tráfico de UAS, robots autónomos y sistemas de detección de fallas. diagnóstico y pronóstico. |
| Nota de contenido: |
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids -- nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement -- Minimum-Violation Traffic Management for Urban Air Mobility -- Integrating Formal Verification and Assurance: An Inspection Rover Case Study -- Towards verifying SHA256 in OpenSSL with the Software Analysis Workbench -- Polygon Merge: A Geometric Algorithm Verified Using PVS -- Program Sketching using Lifted Analysis for Numerical Program Families -- Specification Decomposition for Reactive Synthesis -- On Symmetry and Quantification: A New Approach to Verify Distributed Protocols -- Integrating Runtime Verification into a Sounding Rocket Control System -- Verification of Functional Correctness of Code Diversi cation Techniques -- Scalable Reliability Analysis by Lazy Verification -- Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty -- Good fences make good neighbors: Using formally verified safe trajectories to design a predictive geofence algorithm -- Online Shielding for Stochastic Systems -- Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model -- An Infrastructure for Faithful Execution of Remote Attestation Protocols -- Verifying min-plus Computations with Coq -- Efficient Verification of Optimized Code: Correct High-speed X25519 -- A formal proof of the Lax equivalence theorem for finite difference schemes -- Recursive Variable-Length State Compression for Multi-Core Software Model Checking -- Runtime Verification of Generalized Test Tables -- Quasi-Equal Clock Reduction On-the-Fly -- On the Effectiveness of Signal Rescaling in Hybrid System Falsification. |
| 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 |
13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings [documento electrónico] / Dutle, Aaron, ; Moscato, Mariano M., ; Titolo, Laura, ; Muñoz, César A., ; Perez, Ivan, . - 1 ed. . - [s.l.] : Springer, 2021 . - XVI, 402 p. 133 ilustraciones, 80 ilustraciones en color. ISBN : 978-3-030-76384-8 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 Ingeniería Informática Red de computadoras Inteligencia artificial Simulación por ordenador Teoría de la Computación Ingeniería Informática y Redes Modelado por computadora |
| Índice Dewey: |
005.1 Programación (Computadoras) |
| Resumen: |
Este libro constituye las actas del 13.º Simposio Internacional sobre Métodos Formales de la NASA, NFM 2021, celebrado virtualmente en mayo de 2021. Los 21 artículos completos y 3 breves presentados en este volumen fueron cuidadosamente revisados y seleccionados entre 66 presentaciones. Los documentos tienen como objetivo identificar desafíos y proporcionar soluciones para lograr garantía en sistemas de misión crítica y seguridad crítica. Ejemplos de tales sistemas incluyen algoritmos avanzados de garantía de separación para aeronaves, transporte aéreo de próxima generación, encuentro y acoplamiento autónomo de naves espaciales, software a bordo para sistemas aéreos no tripulados (UAS), gestión del tráfico de UAS, robots autónomos y sistemas de detección de fallas. diagnóstico y pronóstico. |
| Nota de contenido: |
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids -- nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement -- Minimum-Violation Traffic Management for Urban Air Mobility -- Integrating Formal Verification and Assurance: An Inspection Rover Case Study -- Towards verifying SHA256 in OpenSSL with the Software Analysis Workbench -- Polygon Merge: A Geometric Algorithm Verified Using PVS -- Program Sketching using Lifted Analysis for Numerical Program Families -- Specification Decomposition for Reactive Synthesis -- On Symmetry and Quantification: A New Approach to Verify Distributed Protocols -- Integrating Runtime Verification into a Sounding Rocket Control System -- Verification of Functional Correctness of Code Diversi cation Techniques -- Scalable Reliability Analysis by Lazy Verification -- Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty -- Good fences make good neighbors: Using formally verified safe trajectories to design a predictive geofence algorithm -- Online Shielding for Stochastic Systems -- Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model -- An Infrastructure for Faithful Execution of Remote Attestation Protocols -- Verifying min-plus Computations with Coq -- Efficient Verification of Optimized Code: Correct High-speed X25519 -- A formal proof of the Lax equivalence theorem for finite difference schemes -- Recursive Variable-Length State Compression for Multi-Core Software Model Checking -- Runtime Verification of Generalized Test Tables -- Quasi-Equal Clock Reduction On-the-Fly -- On the Effectiveness of Signal Rescaling in Hybrid System Falsification. |
| 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 |
|  |