Información del autor
Autor Hou, Zhe |
Documentos disponibles escritos por este autor (3)
Crear una solicitud de compra Refinar búsqueda
TÃtulo : Automated Technology for Verification and Analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings / Tipo de documento: documento electrónico Autores: Hou, Zhe, ; Ganesh, Vijay, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2021 Número de páginas: XV, 382 p. 103 ilustraciones, 49 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-88885-5 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 Inteligencia artificial Ordenadores IngenierÃa Informática Red de computadoras Hardware de la computadora IngenierÃa Informática y Redes Clasificación: 005.1 Resumen: Este libro constituye las actas arbitradas del 19.º Simposio Internacional sobre TecnologÃa Automatizada para la Verificación y el Análisis, ATVA 2021, celebrado en Gold Coast, Australia, en octubre de 2021. El simposio está dedicado a promover la investigación en aspectos teóricos y prácticos del análisis, la verificación y la automatización. sÃntesis al proporcionar un lugar internacional para que los investigadores presenten nuevos resultados. Los 19 artÃculos regulares presentados junto con 4 artÃculos de herramientas y 1 artÃculo invitado fueron cuidadosamente revisados ​​y seleccionados entre 75 presentaciones. Los artÃculos se dividen en los siguientes subtÃtulos temáticos: TeorÃa de autómatas; Aprendizaje automático para métodos formales; demostración de teoremas y herramientas; Comprobación de modelos; Análisis ProbabilÃstico; Verificación de Software y Hardware; SÃntesis y Aproximación de Sistemas; y Verificación del Aprendizaje Automático. Nota de contenido: Invited Paper -- Linear Temporal Logic  – From Infinite to Finite Horizon -- Automata Theory -- Determinization and Limit-determinization of Emerson-Lei automata -- Automatic discovery of fair paths in infinite-state transition systems -- Certifying DFA Bounds for Recognition and Separation -- Machine Learning for Formal Methods -- AALpy: An Active Automata Learning Library -- Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach -- Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems -- Theorem Proving and Tools -- A Formal Semantics of the GraalVM Intermediate Representation -- A Verified Decision Procedure for Orders in Isabelle/HOL -- PJBDD: A BDD Library for Java and Multi-Threading -- Model Checking -- Live Synthesis -- Faster Pushdown Reachability Analysis with Applications in Network Verification -- Verifying Verified Code -- Probabilistic Analysis -- Probabilistic causes in Markov Chains -- TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments -- AQUA: Automated Quantized Inference for Probabilistic Programs -- Software and Hardware Verification -- Proving SIFA Protection of Masked Redundant Circuits -- Verification by Gambling on Program Slices -- Runtime Enforcement of Hyperproperties -- System Synthesis and Approximation -- Compositional Synthesis of Modular Systems -- Event-B Refinement for Continuous Behaviours Approximation -- Incorporating Monitors in Reactive Synthesis without Paying the Price -- Verification of Machine Learning -- pyNever: a Framework for Learning and Verification of Neural Networks -- Property-Directed Verification and Robustness Certification of Recurrent Neural Networks. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, held in Gold Coast, Australia in October 2021. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 19 regular papers presented together with 4 tool papers and 1 invited paper were carefully reviewed and selected from 75 submissions. The papers are divided into the following topical sub-headings: Automata Theory; Machine learning for Formal Methods; Theorem Proving and Tools; Model Checking; Probabilistic Analysis; Software and Hardware Verification; System Synthesis and Approximation; and Verification of Machine Learning. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Automated Technology for Verification and Analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings / [documento electrónico] / Hou, Zhe, ; Ganesh, Vijay, . - 1 ed. . - [s.l.] : Springer, 2021 . - XV, 382 p. 103 ilustraciones, 49 ilustraciones en color.
ISBN : 978-3-030-88885-5
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 Inteligencia artificial Ordenadores IngenierÃa Informática Red de computadoras Hardware de la computadora IngenierÃa Informática y Redes Clasificación: 005.1 Resumen: Este libro constituye las actas arbitradas del 19.º Simposio Internacional sobre TecnologÃa Automatizada para la Verificación y el Análisis, ATVA 2021, celebrado en Gold Coast, Australia, en octubre de 2021. El simposio está dedicado a promover la investigación en aspectos teóricos y prácticos del análisis, la verificación y la automatización. sÃntesis al proporcionar un lugar internacional para que los investigadores presenten nuevos resultados. Los 19 artÃculos regulares presentados junto con 4 artÃculos de herramientas y 1 artÃculo invitado fueron cuidadosamente revisados ​​y seleccionados entre 75 presentaciones. Los artÃculos se dividen en los siguientes subtÃtulos temáticos: TeorÃa de autómatas; Aprendizaje automático para métodos formales; demostración de teoremas y herramientas; Comprobación de modelos; Análisis ProbabilÃstico; Verificación de Software y Hardware; SÃntesis y Aproximación de Sistemas; y Verificación del Aprendizaje Automático. Nota de contenido: Invited Paper -- Linear Temporal Logic  – From Infinite to Finite Horizon -- Automata Theory -- Determinization and Limit-determinization of Emerson-Lei automata -- Automatic discovery of fair paths in infinite-state transition systems -- Certifying DFA Bounds for Recognition and Separation -- Machine Learning for Formal Methods -- AALpy: An Active Automata Learning Library -- Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach -- Mining Interpretable Spatio-temporal Logic Properties for Spatially Distributed Systems -- Theorem Proving and Tools -- A Formal Semantics of the GraalVM Intermediate Representation -- A Verified Decision Procedure for Orders in Isabelle/HOL -- PJBDD: A BDD Library for Java and Multi-Threading -- Model Checking -- Live Synthesis -- Faster Pushdown Reachability Analysis with Applications in Network Verification -- Verifying Verified Code -- Probabilistic Analysis -- Probabilistic causes in Markov Chains -- TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments -- AQUA: Automated Quantized Inference for Probabilistic Programs -- Software and Hardware Verification -- Proving SIFA Protection of Masked Redundant Circuits -- Verification by Gambling on Program Slices -- Runtime Enforcement of Hyperproperties -- System Synthesis and Approximation -- Compositional Synthesis of Modular Systems -- Event-B Refinement for Continuous Behaviours Approximation -- Incorporating Monitors in Reactive Synthesis without Paying the Price -- Verification of Machine Learning -- pyNever: a Framework for Learning and Verification of Neural Networks -- Property-Directed Verification and Robustness Certification of Recurrent Neural Networks. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, held in Gold Coast, Australia in October 2021. The symposium is dedicated to promoting research in theoretical and practical aspects of automated analysis, verification and synthesis by providing an international venue for the researchers to present new results. The 19 regular papers presented together with 4 tool papers and 1 invited paper were carefully reviewed and selected from 75 submissions. The papers are divided into the following topical sub-headings: Automata Theory; Machine learning for Formal Methods; Theorem Proving and Tools; Model Checking; Probabilistic Analysis; Software and Hardware Verification; System Synthesis and Approximation; and Verification of Machine Learning. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
TÃtulo : Formal Methods and Software Engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings / Tipo de documento: documento electrónico Autores: Lin, Shang-Wei, ; Hou, Zhe, ; Mahony, Brendan, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2020 Número de páginas: XI, 335 p. 98 ilustraciones, 48 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-63406-3 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: Ciencias de la Computación IngenierÃa de software Software de la aplicacion Compiladores (programas informáticos) Programación lógica Procesamiento del lenguaje natural (Informática) TeorÃa de la Computación Aplicaciones informáticas y de sistemas de información Compiladores e intérpretes Lógica en IA Procesamiento del lenguaje natural (PNL) Clasificación: 40.151 Resumen: Este libro constituye las actas de la 22.ª Conferencia Internacional sobre Métodos de IngenierÃa Formal, ICFEM 2020, celebrada en Singapur, Singapur, en marzo de 2021. Los 16 artÃculos completos y 4 breves presentados junto con 1 artÃculo de simposio doctoral en este volumen fueron cuidadosamente revisados ​​y seleccionados. de 41 presentaciones. Los artÃculos cubren la teorÃa y las aplicaciones de los métodos formales de ingenierÃa junto con estudios de casos. También representan el desarrollo reciente en el uso y desarrollo de métodos formales de ingenierÃa para el desarrollo de software y sistemas. Nota de contenido: Safety and Security -- Program Verification -- Formal Methods and Machine Learning -- Formal Languages -- Other Applications of Formal Methods. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 22nd International Conference on Formal Engineering Methods, ICFEM 2020, held in Singapore, Singapore, in March 2021. The 16 full and 4 short papers presented together with 1 doctoral symposium paper in this volume were carefully reviewed and selected from 41 submissions. The papers cover theory and applications in formal engineering methods together with case studies. They also represent the recent development in the use and development of formal engineering methods for software and system development. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Formal Methods and Software Engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings / [documento electrónico] / Lin, Shang-Wei, ; Hou, Zhe, ; Mahony, Brendan, . - 1 ed. . - [s.l.] : Springer, 2020 . - XI, 335 p. 98 ilustraciones, 48 ilustraciones en color.
ISBN : 978-3-030-63406-3
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: Ciencias de la Computación IngenierÃa de software Software de la aplicacion Compiladores (programas informáticos) Programación lógica Procesamiento del lenguaje natural (Informática) TeorÃa de la Computación Aplicaciones informáticas y de sistemas de información Compiladores e intérpretes Lógica en IA Procesamiento del lenguaje natural (PNL) Clasificación: 40.151 Resumen: Este libro constituye las actas de la 22.ª Conferencia Internacional sobre Métodos de IngenierÃa Formal, ICFEM 2020, celebrada en Singapur, Singapur, en marzo de 2021. Los 16 artÃculos completos y 4 breves presentados junto con 1 artÃculo de simposio doctoral en este volumen fueron cuidadosamente revisados ​​y seleccionados. de 41 presentaciones. Los artÃculos cubren la teorÃa y las aplicaciones de los métodos formales de ingenierÃa junto con estudios de casos. También representan el desarrollo reciente en el uso y desarrollo de métodos formales de ingenierÃa para el desarrollo de software y sistemas. Nota de contenido: Safety and Security -- Program Verification -- Formal Methods and Machine Learning -- Formal Languages -- Other Applications of Formal Methods. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 22nd International Conference on Formal Engineering Methods, ICFEM 2020, held in Singapore, Singapore, in March 2021. The 16 full and 4 short papers presented together with 1 doctoral symposium paper in this volume were carefully reviewed and selected from 41 submissions. The papers cover theory and applications in formal engineering methods together with case studies. They also represent the recent development in the use and development of formal engineering methods for software and system development. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
TÃtulo : Fundamentals of Logic and Computation : With Practical Automated Reasoning and Verification Tipo de documento: documento electrónico Autores: Hou, Zhe, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2021 Número de páginas: X, 222 p. 34 ilustraciones, 6 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-87882-5 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: Unidades aritméticas y lógicas informáticas. Ciencias de la Computación TeorÃa de las máquinas Ordenadores Estructuras aritméticas y lógicas TeorÃa de la Computación Lenguajes formales y teorÃa de los autómatas Rendimiento y confiabilidad del hardware Clasificación: 004.01513 Resumen: Aunque los campos de la lógica y la computación están intrÃnsecamente relacionados, la mayorÃa de los cursos tratan los dos temas por separado. Este libro de texto único tiene como objetivo comprimir y unificar conceptos importantes de razonamiento lógico y teorÃa computacional, facilitando una comprensión profunda. El libro, que ofrece teorÃa con enfoques prácticos, presenta los primeros capÃtulos acompañados de ejercicios en Isabelle/HOL, un demostrador de teoremas popular y fácil de usar. Los últimos capÃtulos abordan el modelado y la verificación en Process Analysis Toolkit (PAT), un verificador de modelos rico en funciones basado en Communicating Sequential Processes de Hoare. La exposición se centra en la sintaxis, la semántica y la teorÃa de la prueba de diversas lógicas, asà como en la teorÃa de los autómatas, los lenguajes formales, la computabilidad y la complejidad. También desarrolla un conjunto hÃbrido de habilidades de demostración práctica de teoremas y verificación de modelos, que proporcionará una base sólida para futuras investigaciones o trabajos que involucren métodos formales. Temas y caracterÃsticas: Ofrece una transición de la lógica a la computación a través de lógica temporal lineal y máquinas de estado Incluye ejercicios de aplicaciones de software ampliamente utilizadas Proporciona tutoriales de nivel básico para Isabelle/HOL y PAT Emplea muchos ejemplos de Archives of Formal Proofs, asà como muchos ejemplos de modelos PAT Presenta la lógica clásica y no clásica en una presentación integrada Analiza el cálculo lambda, funciones recursivas y máquinas de Turing Concluye abordando la correspondencia Curry-Howard, que unifica la lógica y la computación El trabajo es óptimo para estudiantes universitarios que aspiran a obtener un tÃtulo en informática . Además, será un volumen fundamental excelente para estudiantes de investigación que estén considerando programas de investigación de grado superior. Zhe Hou es profesora en la Escuela de TecnologÃa de la Información y las Comunicaciones de la Universidad Griffith, Nathan, Australia. Sus lÃneas de investigación incluyen IA explicable, sistemas autónomos, verificación formal y razonamiento automatizado. Nota de contenido: 1. Introduction to Logic -- 2. First-order Logic -- 3. Non-classical Logics -- 4. Automata Theory and Formal Languages -- 5. Turing Machines and Computability -- 6. Logic is Computation. Tipo de medio : Computadora Summary : Although the fields of logic and computation are intrinsically related, most courses treat the two topics separately. This unique textbook aims to compress and unify important concepts of logical reasoning and computational theory, facilitating an in-depth understanding. Delivering theory with practical approaches, the book features early chapters accompanied by exercises in Isabelle/HOL, a popular and user-friendly theorem prover. Latter chapters address modelling and verification in Process Analysis Toolkit (PAT), a feature-rich model checker based on Hoare's Communicating Sequential Processes. The exposition focuses on the syntax, semantics and proof theory of various logics, as well as on automata theory, formal languages, computability, and complexity. It also builds a hybrid skill set of practical theorem proving and model checking, which will provide a solid grounding for future research or work involving formal methods. Topicsand features: Offers a transition from logic to computation via linear temporal logic and state machines Includes exercises from widely-used software applications Provides entry-level tutorials for Isabelle/HOL and PAT Employs many examples from the Archives of Formal Proofs, as well as many examples of PAT models Introduces classical and nonclassical logics in an integrated presentation Discusses lambda calculus, recursive functions and Turing machines Concludes by addressing the Curry-Howard correspondence, which unifies logic and computation The work is optimal for undergraduate students striving for a degree in computer science. In addition, it will be an excellent foundational volume for research students considering higher-degree research programs. Zhe Hou is a lecturer in the School of Information and Communication Technology at Griffith University, Nathan, Australia. His research pursuits include explainable AI, autonomous systems, formal verification, and automated reasoning. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Fundamentals of Logic and Computation : With Practical Automated Reasoning and Verification [documento electrónico] / Hou, Zhe, . - 1 ed. . - [s.l.] : Springer, 2021 . - X, 222 p. 34 ilustraciones, 6 ilustraciones en color.
ISBN : 978-3-030-87882-5
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: Unidades aritméticas y lógicas informáticas. Ciencias de la Computación TeorÃa de las máquinas Ordenadores Estructuras aritméticas y lógicas TeorÃa de la Computación Lenguajes formales y teorÃa de los autómatas Rendimiento y confiabilidad del hardware Clasificación: 004.01513 Resumen: Aunque los campos de la lógica y la computación están intrÃnsecamente relacionados, la mayorÃa de los cursos tratan los dos temas por separado. Este libro de texto único tiene como objetivo comprimir y unificar conceptos importantes de razonamiento lógico y teorÃa computacional, facilitando una comprensión profunda. El libro, que ofrece teorÃa con enfoques prácticos, presenta los primeros capÃtulos acompañados de ejercicios en Isabelle/HOL, un demostrador de teoremas popular y fácil de usar. Los últimos capÃtulos abordan el modelado y la verificación en Process Analysis Toolkit (PAT), un verificador de modelos rico en funciones basado en Communicating Sequential Processes de Hoare. La exposición se centra en la sintaxis, la semántica y la teorÃa de la prueba de diversas lógicas, asà como en la teorÃa de los autómatas, los lenguajes formales, la computabilidad y la complejidad. También desarrolla un conjunto hÃbrido de habilidades de demostración práctica de teoremas y verificación de modelos, que proporcionará una base sólida para futuras investigaciones o trabajos que involucren métodos formales. Temas y caracterÃsticas: Ofrece una transición de la lógica a la computación a través de lógica temporal lineal y máquinas de estado Incluye ejercicios de aplicaciones de software ampliamente utilizadas Proporciona tutoriales de nivel básico para Isabelle/HOL y PAT Emplea muchos ejemplos de Archives of Formal Proofs, asà como muchos ejemplos de modelos PAT Presenta la lógica clásica y no clásica en una presentación integrada Analiza el cálculo lambda, funciones recursivas y máquinas de Turing Concluye abordando la correspondencia Curry-Howard, que unifica la lógica y la computación El trabajo es óptimo para estudiantes universitarios que aspiran a obtener un tÃtulo en informática . Además, será un volumen fundamental excelente para estudiantes de investigación que estén considerando programas de investigación de grado superior. Zhe Hou es profesora en la Escuela de TecnologÃa de la Información y las Comunicaciones de la Universidad Griffith, Nathan, Australia. Sus lÃneas de investigación incluyen IA explicable, sistemas autónomos, verificación formal y razonamiento automatizado. Nota de contenido: 1. Introduction to Logic -- 2. First-order Logic -- 3. Non-classical Logics -- 4. Automata Theory and Formal Languages -- 5. Turing Machines and Computability -- 6. Logic is Computation. Tipo de medio : Computadora Summary : Although the fields of logic and computation are intrinsically related, most courses treat the two topics separately. This unique textbook aims to compress and unify important concepts of logical reasoning and computational theory, facilitating an in-depth understanding. Delivering theory with practical approaches, the book features early chapters accompanied by exercises in Isabelle/HOL, a popular and user-friendly theorem prover. Latter chapters address modelling and verification in Process Analysis Toolkit (PAT), a feature-rich model checker based on Hoare's Communicating Sequential Processes. The exposition focuses on the syntax, semantics and proof theory of various logics, as well as on automata theory, formal languages, computability, and complexity. It also builds a hybrid skill set of practical theorem proving and model checking, which will provide a solid grounding for future research or work involving formal methods. Topicsand features: Offers a transition from logic to computation via linear temporal logic and state machines Includes exercises from widely-used software applications Provides entry-level tutorials for Isabelle/HOL and PAT Employs many examples from the Archives of Formal Proofs, as well as many examples of PAT models Introduces classical and nonclassical logics in an integrated presentation Discusses lambda calculus, recursive functions and Turing machines Concludes by addressing the Curry-Howard correspondence, which unifies logic and computation The work is optimal for undergraduate students striving for a degree in computer science. In addition, it will be an excellent foundational volume for research students considering higher-degree research programs. Zhe Hou is a lecturer in the School of Information and Communication Technology at Griffith University, Nathan, Australia. His research pursuits include explainable AI, autonomous systems, formal verification, and automated reasoning. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
