Información del autor
Autor Muñoz, César A. |
Documentos disponibles escritos por este autor (2)
Crear una solicitud de compra Refinar búsqueda
TÃtulo : Interactive Theorem Proving : 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. Idioma : Inglés (eng) 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 Clasificación: 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. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Interactive Theorem Proving : 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.
Idioma : Inglés (eng)
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 Clasificación: 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. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] NASA Formal Methods / Dutle, Aaron ; Moscato, Mariano M. ; Titolo, Laura ; Muñoz, César A. ; Perez, Ivan
TÃtulo : NASA Formal Methods : 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. Idioma : Inglés (eng) 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 Clasificación: 005.1 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. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, held virtually in May 2021. The 21 full and 3 short papers presented in this volume were carefully reviewed and selected from 66 submissions. The papers aim to identify challenges and provide solutions to achieve assurance in mission-critical and safety-critical systems. Examples of such systems include advanced separation assurance algorithms for aircraft, next-generation air transportation, autonomous rendezvous and docking of spacecraft, on-board software for unmanned aerial systems (UAS), UAS traffic management, autonomous robots, and systems for fault detection, diagnosis, and prognostics. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] NASA Formal Methods : 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.
Idioma : Inglés (eng)
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 Clasificación: 005.1 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. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, held virtually in May 2021. The 21 full and 3 short papers presented in this volume were carefully reviewed and selected from 66 submissions. The papers aim to identify challenges and provide solutions to achieve assurance in mission-critical and safety-critical systems. Examples of such systems include advanced separation assurance algorithms for aircraft, next-generation air transportation, autonomous rendezvous and docking of spacecraft, on-board software for unmanned aerial systems (UAS), UAS traffic management, autonomous robots, and systems for fault detection, diagnosis, and prognostics. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
