| TÃtulo : |
Tools and Algorithms for the Construction and Analysis of Systems : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II |
| Tipo de documento: |
documento electrónico |
| Autores: |
Legay, Axel, ; Margaria, Tiziana, |
| Mención de edición: |
1 ed. |
| Editorial: |
Berlin [Alemania] : Springer |
| Fecha de publicación: |
2017 |
| Número de páginas: |
XXIV, 411 p. 88 ilustraciones |
| ISBN/ISSN/DL: |
978-3-662-54580-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: |
Ciencias de la Computación Algoritmos IngenierÃa de software Compiladores (programas informáticos) TeorÃa de las máquinas Lógica informática y fundamentos de la programación TeorÃa de la Computación Compiladores e intérpretes Lenguajes formales y teorÃa de los autómatas |
| Ãndice Dewey: |
40.151 |
| Resumen: |
El conjunto de dos libros LNCS 10205 + 10206 constituye las actas de la 23.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas, TACAS 2017, que tuvo lugar en Uppsala, Suecia, en abril de 2017, como parte del Congreso Conjunto Europeo. Conferencias sobre teorÃa y práctica del software, ETAPS 2017. Los 48 artÃculos completos, 4 artÃculos de demostración de herramientas y 12 artÃculos de competencia de software presentados en estos volúmenes fueron cuidadosamente revisados ​​y seleccionados entre 181 presentaciones a TACAS y 32 presentaciones a la competencia de software. Fueron organizados en secciones temáticas denominadas: técnicas de verificación; aprendiendo; sÃntesis; autómatas; concurrencia y bisimulación; sistemas hÃbridos; seguridad; verificación y lógica en tiempo de ejecución; sistemas cuantitativos; SAT y SMT; y SV COMP. . |
| Nota de contenido: |
Security -- Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions -- Discriminating Traces with Time -- Directed Automated Memory Performance Testing -- Context-bounded Analysis for POWER -- Run-Time Verification and Logic. -Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas -- Almost Event-Rate Independent Monitoring of Metric Temporal Logic -- Optimal Translation of LTL to Limit Deterministic Automata -- Quantitative Systems -- Sequential Convex Programming for the Efficient Verification of Parametric MDPs -- JANI: Quantitative Model and Tool Interaction -- Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults -- Long-run Rewards for Markov Automata -- SAT and SMT -- HiFrog: SMT-based Function Summarization for Software Verification -- Congruence Closure with Free Variables -- On Optimization Modulo Theories, MaxSMT and Sorting Networks. - The automatic detection of token structures and invariants using SAT checking -- Maximizing the Conditional Expected Reward for Reaching the Goal. -ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - FlyFast: A Mean Field Model Checker. -ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations.-SV COMP -- Software Verification with Validation of Results (Report on SV-COMP 2017) -- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution) -- CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions (Competition Contribution) -- DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution) -- Forester: From Heap Shapes to Automata Predicates (Competition Contribution) -- HipTNT+: A Termination and Non-termination Analyzer by Second-order Abduction (Competition Contribution) -- Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution) -- Skink: Static Analysis of LLVM Intermediate Representation (Competition contribution) -- Symbiotic 4: Beyond Reachability (Competition Contribution) -- Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution) -- Ultimate Automizer with an On-demand Construction of Floyd-Hoare Automata (Competition Contribution) -- Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution) -- VeriAbs : 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 |
Tools and Algorithms for the Construction and Analysis of Systems : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II [documento electrónico] / Legay, Axel, ; Margaria, Tiziana, . - 1 ed. . - Berlin [Alemania] : Springer, 2017 . - XXIV, 411 p. 88 ilustraciones. ISBN : 978-3-662-54580-5 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 Algoritmos IngenierÃa de software Compiladores (programas informáticos) TeorÃa de las máquinas Lógica informática y fundamentos de la programación TeorÃa de la Computación Compiladores e intérpretes Lenguajes formales y teorÃa de los autómatas |
| Ãndice Dewey: |
40.151 |
| Resumen: |
El conjunto de dos libros LNCS 10205 + 10206 constituye las actas de la 23.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas, TACAS 2017, que tuvo lugar en Uppsala, Suecia, en abril de 2017, como parte del Congreso Conjunto Europeo. Conferencias sobre teorÃa y práctica del software, ETAPS 2017. Los 48 artÃculos completos, 4 artÃculos de demostración de herramientas y 12 artÃculos de competencia de software presentados en estos volúmenes fueron cuidadosamente revisados ​​y seleccionados entre 181 presentaciones a TACAS y 32 presentaciones a la competencia de software. Fueron organizados en secciones temáticas denominadas: técnicas de verificación; aprendiendo; sÃntesis; autómatas; concurrencia y bisimulación; sistemas hÃbridos; seguridad; verificación y lógica en tiempo de ejecución; sistemas cuantitativos; SAT y SMT; y SV COMP. . |
| Nota de contenido: |
Security -- Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions -- Discriminating Traces with Time -- Directed Automated Memory Performance Testing -- Context-bounded Analysis for POWER -- Run-Time Verification and Logic. -Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas -- Almost Event-Rate Independent Monitoring of Metric Temporal Logic -- Optimal Translation of LTL to Limit Deterministic Automata -- Quantitative Systems -- Sequential Convex Programming for the Efficient Verification of Parametric MDPs -- JANI: Quantitative Model and Tool Interaction -- Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults -- Long-run Rewards for Markov Automata -- SAT and SMT -- HiFrog: SMT-based Function Summarization for Software Verification -- Congruence Closure with Free Variables -- On Optimization Modulo Theories, MaxSMT and Sorting Networks. - The automatic detection of token structures and invariants using SAT checking -- Maximizing the Conditional Expected Reward for Reaching the Goal. -ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - FlyFast: A Mean Field Model Checker. -ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations.-SV COMP -- Software Verification with Validation of Results (Report on SV-COMP 2017) -- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution) -- CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions (Competition Contribution) -- DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution) -- Forester: From Heap Shapes to Automata Predicates (Competition Contribution) -- HipTNT+: A Termination and Non-termination Analyzer by Second-order Abduction (Competition Contribution) -- Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution) -- Skink: Static Analysis of LLVM Intermediate Representation (Competition contribution) -- Symbiotic 4: Beyond Reachability (Competition Contribution) -- Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution) -- Ultimate Automizer with an On-demand Construction of Floyd-Hoare Automata (Competition Contribution) -- Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution) -- VeriAbs : 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 |
|  |
Tools and Algorithms for the Construction and Analysis of Systems
