Título :	27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II
Tipo de documento:	documento electrónico
Autores:	Groote, Jan Friso, ; Larsen, Kim Guldstrand,
Mención de edición:	1 ed.
Editorial:	[s.l.] : Springer
Fecha de publicación:	2021
Número de páginas:	XXI, 465 p. 91 ilustraciones
ISBN/ISSN/DL:	978-3-030-72013-1
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  Microprogramación  Ingeniería de software  Teoría de la Computación  Ingeniería Informática y Redes  Estructuras de control y microprogramación
Índice Dewey:	40.151
Resumen:	Este conjunto de dos volúmenes de acceso abierto constituye las actas de la 27.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas, TACAS 2021, que se celebró del 27 de marzo al 1 de abril de 2021, como parte de las Conferencias Conjuntas Europeas sobre Teoría y práctica del software, ETAPS 2021. Se planeó que la conferencia se llevara a cabo en Luxemburgo y cambió a un formato en línea debido a la pandemia de COVID-19. El total de 41 artículos completos presentados en las actas fue cuidadosamente revisado y seleccionado entre 141 presentaciones. El volumen también contiene 7 documentos de herramientas; 6 artículos de demostración de herramientas, 9 artículos de competencia SV-Comp. Los artículos están organizados en secciones temáticas de la siguiente manera: Parte I: Teoría de juegos; Verificación SMT; Probabilidades; Sistemas Temporizados; Redes neuronales; Análisis de la Comunicación en Red. Parte II: Técnicas de verificación (no SMT); Estudios de caso; Generación/Validación de Pruebas; Papeles para herramientas; Documentos de demostración de herramientas; Documentos del concurso de herramientas SV-Comp.
Nota de contenido:	Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- Bridging Arrays and ADTs in Recursive Proofs -- A Two-Phase Approach for Conditional Floating-Point Verification -- Symbolic Coloured SCC Decomposition -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- Syntax-Guided Quantifier Instantiation -- Making Theory Reasoning Simpler -- Deductive Stability Proofs for Ordinary Differential Equations -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- cake lpr: Verified Propagation Redundancy Checking in CakeML -- Deductive Veri cation of Floating-Point Java Programs in KeY -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- SyReNN: A Tool for Analyzing Deep Neural Networks -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- AMulet 2.0 for Verifying Multiplier Circuits -- RTLola on Board: Testing Real Driving Emissions on your Phone -- Replicating Restart with Prolonged Retrials: An Experimental Report -- A Web Interface for Petri Nets with Transits and Petri Games -- Momba: JANI Meets Python -- SV-Comp Tool Competition Papers -- Software Veri cation: 10th Comparative Evaluation (SV-COMP 2021) -- CPALockator: Thread-Modular Approach with Projections (Competition Contribution) -- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution) -- Gazer-Theta: LLVM-based Veri er Portfolio with BMC/CEGAR (Competition Contribution) -- Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution) -- Towards String Support in JayHorn (Competition Contribution) -- JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) -- Symbiotic 8: Beyond Symbolic Execution (Competition Contribution) -- VeriAbs: A Tool for Scalable Verification by Abstraction (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

27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II [documento electrónico] / Groote, Jan Friso, ; Larsen, Kim Guldstrand,  . -  1 ed.  . - [s.l.] : Springer, 2021 . - XXI, 465 p. 91 ilustraciones.
ISBN : 978-3-030-72013-1
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  Microprogramación  Ingeniería de software  Teoría de la Computación  Ingeniería Informática y Redes  Estructuras de control y microprogramación
Índice Dewey:	40.151
Resumen:	Este conjunto de dos volúmenes de acceso abierto constituye las actas de la 27.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas, TACAS 2021, que se celebró del 27 de marzo al 1 de abril de 2021, como parte de las Conferencias Conjuntas Europeas sobre Teoría y práctica del software, ETAPS 2021. Se planeó que la conferencia se llevara a cabo en Luxemburgo y cambió a un formato en línea debido a la pandemia de COVID-19. El total de 41 artículos completos presentados en las actas fue cuidadosamente revisado y seleccionado entre 141 presentaciones. El volumen también contiene 7 documentos de herramientas; 6 artículos de demostración de herramientas, 9 artículos de competencia SV-Comp. Los artículos están organizados en secciones temáticas de la siguiente manera: Parte I: Teoría de juegos; Verificación SMT; Probabilidades; Sistemas Temporizados; Redes neuronales; Análisis de la Comunicación en Red. Parte II: Técnicas de verificación (no SMT); Estudios de caso; Generación/Validación de Pruebas; Papeles para herramientas; Documentos de demostración de herramientas; Documentos del concurso de herramientas SV-Comp.
Nota de contenido:	Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- Bridging Arrays and ADTs in Recursive Proofs -- A Two-Phase Approach for Conditional Floating-Point Verification -- Symbolic Coloured SCC Decomposition -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- Syntax-Guided Quantifier Instantiation -- Making Theory Reasoning Simpler -- Deductive Stability Proofs for Ordinary Differential Equations -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- cake lpr: Verified Propagation Redundancy Checking in CakeML -- Deductive Veri cation of Floating-Point Java Programs in KeY -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- SyReNN: A Tool for Analyzing Deep Neural Networks -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- AMulet 2.0 for Verifying Multiplier Circuits -- RTLola on Board: Testing Real Driving Emissions on your Phone -- Replicating Restart with Prolonged Retrials: An Experimental Report -- A Web Interface for Petri Nets with Transits and Petri Games -- Momba: JANI Meets Python -- SV-Comp Tool Competition Papers -- Software Veri cation: 10th Comparative Evaluation (SV-COMP 2021) -- CPALockator: Thread-Modular Approach with Projections (Competition Contribution) -- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution) -- Gazer-Theta: LLVM-based Veri er Portfolio with BMC/CEGAR (Competition Contribution) -- Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution) -- Towards String Support in JayHorn (Competition Contribution) -- JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) -- Symbiotic 8: Beyond Symbolic Execution (Competition Contribution) -- VeriAbs: A Tool for Scalable Verification by Abstraction (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