Autor Beyer, Dirk
|
|
Documentos disponibles escritos por este autor (5)
Hacer una sugerencia Refinar búsqueda13th International Conference, TAP 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9–11, 2019, Proceedings / Beyer, Dirk ; Keller, Chantal
Título : 13th International Conference, TAP 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9–11, 2019, Proceedings Tipo de documento: documento electrónico Autores: Beyer, Dirk, ; Keller, Chantal, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2019 Número de páginas: X, 207 p. 339 ilustraciones, 34 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-31157-5 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 Compiladores (programas informáticos) Ciencias de la Computación Teoría de las máquinas Computadoras digitales electrónicas Compiladores e intérpretes Lógica informática y fundamentos de la programación Lenguajes formales y teoría de los autómatas Rendimiento y evaluación del sistema Índice Dewey: 005.1 Programación (Computadoras) Resumen: Este libro constituye las actas arbitradas de la 13.ª Conferencia Internacional sobre Pruebas y Demostraciones, TAP 2019, celebrada como parte del Tercer Congreso Mundial sobre Métodos Formales 2019, Oporto, Portugal, en octubre de 2019. Los 10 artículos regulares y 2 artículos invitados presentados en Este volumen fue cuidadosamente revisado y seleccionado entre 19 presentaciones. La conferencia TAP promueve la investigación en verificación y métodos formales que apuntan a la interacción de pruebas y pruebas: el avance de técnicas de cada tipo y su combinación, con el objetivo final de mejorar la confiabilidad del software y del sistema. Nota de contenido: When are Software Verification Results Valid for Approximate Hardware -- Testing Robots using CSP -- Constraints in Dynamic Symbolic Execution: Bitvectors or Integers -- Fast, Automatic and Nearly Complete Structural Unit Test Generation Combining Genetic Algorithms and Formal Methods -- Coverage-Based Testing with Symbolic Transition Systems -- BTestBox - A tool for testing B translators and coverage of B models -- Predicting and Testing Latencies with Deep Learning: an IoT Case Study -- Learning Communicating State Machines -- Repairing Timed Automata Clock Guards through Abstraction and Testing -- Proving a Non-Blocking Algorithm for Process Renaming with TLA+ -- Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties -- Property-Based Test Case Generators for Free. 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 Conference, TAP 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9–11, 2019, Proceedings [documento electrónico] / Beyer, Dirk, ; Keller, Chantal, . - 1 ed. . - [s.l.] : Springer, 2019 . - X, 207 p. 339 ilustraciones, 34 ilustraciones en color.
ISBN : 978-3-030-31157-5
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 Compiladores (programas informáticos) Ciencias de la Computación Teoría de las máquinas Computadoras digitales electrónicas Compiladores e intérpretes Lógica informática y fundamentos de la programación Lenguajes formales y teoría de los autómatas Rendimiento y evaluación del sistema Índice Dewey: 005.1 Programación (Computadoras) Resumen: Este libro constituye las actas arbitradas de la 13.ª Conferencia Internacional sobre Pruebas y Demostraciones, TAP 2019, celebrada como parte del Tercer Congreso Mundial sobre Métodos Formales 2019, Oporto, Portugal, en octubre de 2019. Los 10 artículos regulares y 2 artículos invitados presentados en Este volumen fue cuidadosamente revisado y seleccionado entre 19 presentaciones. La conferencia TAP promueve la investigación en verificación y métodos formales que apuntan a la interacción de pruebas y pruebas: el avance de técnicas de cada tipo y su combinación, con el objetivo final de mejorar la confiabilidad del software y del sistema. Nota de contenido: When are Software Verification Results Valid for Approximate Hardware -- Testing Robots using CSP -- Constraints in Dynamic Symbolic Execution: Bitvectors or Integers -- Fast, Automatic and Nearly Complete Structural Unit Test Generation Combining Genetic Algorithms and Formal Methods -- Coverage-Based Testing with Symbolic Transition Systems -- BTestBox - A tool for testing B translators and coverage of B models -- Predicting and Testing Latencies with Deep Learning: an IoT Case Study -- Learning Communicating State Machines -- Repairing Timed Automata Clock Guards through Abstraction and Testing -- Proving a Non-Blocking Algorithm for Process Renaming with TLA+ -- Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties -- Property-Based Test Case Generators for Free. 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 : 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings Tipo de documento: documento electrónico Autores: Beyer, Dirk, ; Zufferey, Damien, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2020 Número de páginas: XIV, 471 p. 109 ilustraciones ISBN/ISSN/DL: 978-3-030-39322-9 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 Informática Red de computadoras Programación lógica Inteligencia artificial Ingeniería de software Lógica informática y fundamentos de la programación Ingeniería Informática y Redes Lógica en IA Ciencia de los datos Índice Dewey: 40.151 Resumen: Este libro constituye las actas de la 21.ª Conferencia Internacional sobre Verificación, Verificación de Modelos e Interpretación de Resumenes, VMCAI 2020. Los 21 artículos presentados en este volumen fueron cuidadosamente revisados a partir de 44 presentaciones. VMCAI proporciona un foro para investigadores de las comunidades de verificación, verificación de modelos e interpretación abstracta, facilitando la interacción, la fertilización cruzada y el avance de métodos híbridos que combinan estas y áreas relacionadas. . Nota de contenido: Witnessing Secure Compilation -- BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results -- Fixing Code That Explodes Under Symbolic Evaluation -- The Correctness of a Code Generator for a Functional Language -- Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification -- Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction -- A Systematic Approach to Abstract Interpretation of Program Transformations -- Sharing ghost variables in a collection of abstract domains -- Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation -- Synthesizing Environment Invariants for Modular Hardware Verification -- Systematic Classi cation of Attackers via Bounded Model Checking -- Cheap CTL Compassion in NuSMV -- A Cooperative Parallelization Approach for Property-Directed k-Induction -- Generalized Property-Directed Reachability for Hybrid Systems -- Language Inclusion for Finite Prime Event Structures -- Promptness and Bounded Fairness in Concurrent and Parameterized Systems -- Solving LIA* Using Approximations -- Formalizing and checking Multilevel Consistency -- Practical Abstractions for Automated Veri cation of Shared-Memory Concurrency -- How to Win First-Order Safety Games -- Improving Parity Game Solvers with Justifications. 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 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings [documento electrónico] / Beyer, Dirk, ; Zufferey, Damien, . - 1 ed. . - [s.l.] : Springer, 2020 . - XIV, 471 p. 109 ilustraciones.
ISBN : 978-3-030-39322-9
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 Informática Red de computadoras Programación lógica Inteligencia artificial Ingeniería de software Lógica informática y fundamentos de la programación Ingeniería Informática y Redes Lógica en IA Ciencia de los datos Índice Dewey: 40.151 Resumen: Este libro constituye las actas de la 21.ª Conferencia Internacional sobre Verificación, Verificación de Modelos e Interpretación de Resumenes, VMCAI 2020. Los 21 artículos presentados en este volumen fueron cuidadosamente revisados a partir de 44 presentaciones. VMCAI proporciona un foro para investigadores de las comunidades de verificación, verificación de modelos e interpretación abstracta, facilitando la interacción, la fertilización cruzada y el avance de métodos híbridos que combinan estas y áreas relacionadas. . Nota de contenido: Witnessing Secure Compilation -- BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results -- Fixing Code That Explodes Under Symbolic Evaluation -- The Correctness of a Code Generator for a Functional Language -- Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification -- Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction -- A Systematic Approach to Abstract Interpretation of Program Transformations -- Sharing ghost variables in a collection of abstract domains -- Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation -- Synthesizing Environment Invariants for Modular Hardware Verification -- Systematic Classi cation of Attackers via Bounded Model Checking -- Cheap CTL Compassion in NuSMV -- A Cooperative Parallelization Approach for Property-Directed k-Induction -- Generalized Property-Directed Reachability for Hybrid Systems -- Language Inclusion for Finite Prime Event Structures -- Promptness and Bounded Fairness in Concurrent and Parameterized Systems -- Solving LIA* Using Approximations -- Formalizing and checking Multilevel Consistency -- Practical Abstractions for Automated Veri cation of Shared-Memory Concurrency -- How to Win First-Order Safety Games -- Improving Parity Game Solvers with Justifications. 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 : Tools and Algorithms for the Construction and Analysis of Systems : 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I Tipo de documento: documento electrónico Autores: Beyer, Dirk, ; Huisman, Marieke, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2018 Número de páginas: XX, 429 p. 93 ilustraciones ISBN/ISSN/DL: 978-3-319-89960-2 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 Ordenadores Estructuras de datos (Informática) Teoría de la información Computadoras digitales electrónicas Lógica informática y fundamentos de la programación Entornos informáticos Estructuras de datos y teoría de la información Rendimiento y evaluación del sistema Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. . Nota de contenido: Theorem Proving -- Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning -- Efficient verification of imperative programs using auto2 -- Frame Inference for Inductive Entailment Proofs in Separation Logic -- Verified Model Checking of Timed Automata -- SAT and SMT I -- Chain Reduction for Binary and Zero-Suppressed Decision Diagrams -- CDCLSym: Introducing E_ective Symmetry Breaking in SAT Solving -- Automatic Generation of Precise and Useful Commutativity Conditions -- Bit-Vector Model Counting using Statistical Estimation -- Deductive Verification -- Hoare Logics for Time Bounds -- A Verified Implementation of the Bounded List Container -- Automating Deductive Verification for Weak-Memory Programs -- Software Verification and Optimisation -- Property Checking Array Programs Using Loop Shrinking -- Invariant Synthesis for Incomplete Verification Engines -- Accelerating Syntax-Guided Invariant Synthesis -- Daisy - Framework for Analysis and Optimization of Numerical Programs -- Model Checking -- Oink: an Implementation and Evaluation of Modern Parity Game Solvers -- More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^3) -- Generation of Minimum Tree-like Witnesses for Existential CTL -- From Natural Projection to Partial Model Checking and Back -- Machine Learning -- ICE-based Refinement Type Discovery for Higher-Order Functional Programs -- Strategy Representation by Decision Trees in Reactive Synthesis -- Feature-Guided Black-Box Safety Testing of Deep Neural Networks. . 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 Tools and Algorithms for the Construction and Analysis of Systems : 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I [documento electrónico] / Beyer, Dirk, ; Huisman, Marieke, . - 1 ed. . - [s.l.] : Springer, 2018 . - XX, 429 p. 93 ilustraciones.
ISBN : 978-3-319-89960-2
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 Ordenadores Estructuras de datos (Informática) Teoría de la información Computadoras digitales electrónicas Lógica informática y fundamentos de la programación Entornos informáticos Estructuras de datos y teoría de la información Rendimiento y evaluación del sistema Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. . Nota de contenido: Theorem Proving -- Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning -- Efficient verification of imperative programs using auto2 -- Frame Inference for Inductive Entailment Proofs in Separation Logic -- Verified Model Checking of Timed Automata -- SAT and SMT I -- Chain Reduction for Binary and Zero-Suppressed Decision Diagrams -- CDCLSym: Introducing E_ective Symmetry Breaking in SAT Solving -- Automatic Generation of Precise and Useful Commutativity Conditions -- Bit-Vector Model Counting using Statistical Estimation -- Deductive Verification -- Hoare Logics for Time Bounds -- A Verified Implementation of the Bounded List Container -- Automating Deductive Verification for Weak-Memory Programs -- Software Verification and Optimisation -- Property Checking Array Programs Using Loop Shrinking -- Invariant Synthesis for Incomplete Verification Engines -- Accelerating Syntax-Guided Invariant Synthesis -- Daisy - Framework for Analysis and Optimization of Numerical Programs -- Model Checking -- Oink: an Implementation and Evaluation of Modern Parity Game Solvers -- More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^3) -- Generation of Minimum Tree-like Witnesses for Existential CTL -- From Natural Projection to Partial Model Checking and Back -- Machine Learning -- ICE-based Refinement Type Discovery for Higher-Order Functional Programs -- Strategy Representation by Decision Trees in Reactive Synthesis -- Feature-Guided Black-Box Safety Testing of Deep Neural Networks. . 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 : Tools and Algorithms for the Construction and Analysis of Systems : 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II Tipo de documento: documento electrónico Autores: Beyer, Dirk, ; Huisman, Marieke, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2018 Número de páginas: XX, 465 p. 92 ilustraciones ISBN/ISSN/DL: 978-3-319-89963-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 Ingeniería Informática Red de computadoras Inteligencia artificial Ordenadores Lógica informática y fundamentos de la programación Ingeniería Informática y Redes Entornos informáticos Hardware de la computadora Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. Nota de contenido: Concurrent and Distributed Systems -- Computing the concurrency threshold of sound free-choice workflow nets -- Fine-Grained Complexity of Safety Verification -- Parameterized verification of synchronization in constrained reconfigurable broadcast networks -- EMME: a formal tool for the ECMAScript Memory Model Evaluation -- SAT and SMT II -- What a Difference a Variable Makes -- Abstraction Refinement for Emptiness Checking of Alternating Data Automata -- Revisiting Enumerative Instantiation -- An Non-linear Arithmetic Procedure for Control-Command Software Verification -- Security and Reactive Systems -- Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection -- Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts -- RVHyper: A Runtime Verification Tool for Temporal Hyperproperties -- The Refinement Calculus of Reactive Systems Toolset -- Static and Dynamic Program Analysis -- TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation -- Optimal Dynamic Partial Order Reduction with Observers -- Structurally Defined Conditional Data-flow Static Analysis -- Geometric Nontermination Arguments -- Hybrid and Stochastic Systems -- Efficient dynamic error reduction for hybrid systems reachability analysis -- AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic -- Multi-Cost Bounded Reachability in MDPs -- A Statistical Model Checker for Nondeterminism and Rare Events -- Temporal logic and mu-calculus -- Permutation Games for the Weakly Aconjunctive mu-Calculus -- Symmetry Reduction for the Local Mu-Calculus -- Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models -- 7th Competition on Software Verification (SV-COMP) -- 2LS: Memory Safety and Non-Termination (Competition contribution) -- Yogar-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement (Competition Contribution) -- CPA-BAM-Slicing: Block-Abstraction Memorization and Slicing with Region-BasedDependency Analysis (Competition Contribution) -- InterpChecker: Reducing State Space via Interpolations (Competition Contribution) -- Map2Check using LLVM and KLEE (Competition Contribution) -- Symbiotic 5: Boosted Instrumentation (Competition Contribution) -- Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution) -- Ultimate Taipan with Dynamic Block Encoding (Competition Contribution) -- VeriAbs : Verification by Abstraction and Test Generation (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 Tools and Algorithms for the Construction and Analysis of Systems : 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II [documento electrónico] / Beyer, Dirk, ; Huisman, Marieke, . - 1 ed. . - [s.l.] : Springer, 2018 . - XX, 465 p. 92 ilustraciones.
ISBN : 978-3-319-89963-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 Ingeniería Informática Red de computadoras Inteligencia artificial Ordenadores Lógica informática y fundamentos de la programación Ingeniería Informática y Redes Entornos informáticos Hardware de la computadora Índice Dewey: 40.151 Resumen: Este libro es de Acceso Abierto bajo licencia CC BY. Nota de contenido: Concurrent and Distributed Systems -- Computing the concurrency threshold of sound free-choice workflow nets -- Fine-Grained Complexity of Safety Verification -- Parameterized verification of synchronization in constrained reconfigurable broadcast networks -- EMME: a formal tool for the ECMAScript Memory Model Evaluation -- SAT and SMT II -- What a Difference a Variable Makes -- Abstraction Refinement for Emptiness Checking of Alternating Data Automata -- Revisiting Enumerative Instantiation -- An Non-linear Arithmetic Procedure for Control-Command Software Verification -- Security and Reactive Systems -- Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection -- Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts -- RVHyper: A Runtime Verification Tool for Temporal Hyperproperties -- The Refinement Calculus of Reactive Systems Toolset -- Static and Dynamic Program Analysis -- TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation -- Optimal Dynamic Partial Order Reduction with Observers -- Structurally Defined Conditional Data-flow Static Analysis -- Geometric Nontermination Arguments -- Hybrid and Stochastic Systems -- Efficient dynamic error reduction for hybrid systems reachability analysis -- AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic -- Multi-Cost Bounded Reachability in MDPs -- A Statistical Model Checker for Nondeterminism and Rare Events -- Temporal logic and mu-calculus -- Permutation Games for the Weakly Aconjunctive mu-Calculus -- Symmetry Reduction for the Local Mu-Calculus -- Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models -- 7th Competition on Software Verification (SV-COMP) -- 2LS: Memory Safety and Non-Termination (Competition contribution) -- Yogar-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement (Competition Contribution) -- CPA-BAM-Slicing: Block-Abstraction Memorization and Slicing with Region-BasedDependency Analysis (Competition Contribution) -- InterpChecker: Reducing State Space via Interpolations (Competition Contribution) -- Map2Check using LLVM and KLEE (Competition Contribution) -- Symbiotic 5: Boosted Instrumentation (Competition Contribution) -- Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution) -- Ultimate Taipan with Dynamic Block Encoding (Competition Contribution) -- VeriAbs : Verification by Abstraction and Test Generation (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
