Autor Muñoz, César A.
|
|
Documentos disponibles escritos por este autor (2)
Hacer una sugerencia Refinar búsqueda13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Proceedings / Dutle, Aaron ; Moscato, Mariano M. ; Titolo, Laura ; Muñoz, César A. ; Perez, Ivan
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
Título : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings Tipo de documento: documento electrónico Autores: Ayala-Rincón, Mauricio, ; Muñoz, César A., Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2017 Número de páginas: XIX, 532 p. 79 ilustraciones ISBN/ISSN/DL: 978-3-319-66107-0 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: Informática Lenguajes formales y teoría de los autómatas Inteligencia artificial Compiladores e intérpretes Ingeniería de software Rendimiento y evaluación del sistema Lógica informática y fundamentos de la programación Compiladores (programas informáticos) Computadoras digitales electrónicas Teoría de las máquinas Evaluación Índice Dewey: 5.131 Resumen: Este libro constituye las actas arbitradas de la 8.ª Conferencia Internacional sobre Demostración Interactiva de Teoremas, ITP 2017, celebrada en Brasilia, Brasil, en septiembre de 2017. Los 28 artículos completos, 2 artículos sobre diamantes en bruto y 3 artículos de discusión invitados presentados fueron cuidadosamente revisados y seleccionados. de 65 presentaciones. Los temas abarcan desde fundamentos teóricos hasta aspectos de implementación y aplicaciones en la verificación de programas, seguridad y formalización de teorías matemáticas. Nota de contenido: Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of theFundamental Group in Untyped Set Theory Using auto2. 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 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings [documento electrónico] / Ayala-Rincón, Mauricio, ; Muñoz, César A., . - 1 ed. . - [s.l.] : Springer, 2017 . - XIX, 532 p. 79 ilustraciones.
ISBN : 978-3-319-66107-0
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Palabras clave: Informática Lenguajes formales y teoría de los autómatas Inteligencia artificial Compiladores e intérpretes Ingeniería de software Rendimiento y evaluación del sistema Lógica informática y fundamentos de la programación Compiladores (programas informáticos) Computadoras digitales electrónicas Teoría de las máquinas Evaluación Índice Dewey: 5.131 Resumen: Este libro constituye las actas arbitradas de la 8.ª Conferencia Internacional sobre Demostración Interactiva de Teoremas, ITP 2017, celebrada en Brasilia, Brasil, en septiembre de 2017. Los 28 artículos completos, 2 artículos sobre diamantes en bruto y 3 artículos de discusión invitados presentados fueron cuidadosamente revisados y seleccionados. de 65 presentaciones. Los temas abarcan desde fundamentos teóricos hasta aspectos de implementación y aplicaciones en la verificación de programas, seguridad y formalización de teorías matemáticas. Nota de contenido: Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of theFundamental Group in Untyped Set Theory Using auto2. 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
