TÃtulo : |
12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20–21, 2020, Revised Selected Papers |
Tipo de documento: |
documento electrónico |
Autores: |
Christakis, Maria, ; Polikarpova, Nadia, ; Duggirala, Parasara Sridhar, ; Schrammel, Peter, |
Mención de edición: |
1 ed. |
Editorial: |
[s.l.] : Springer |
Fecha de publicación: |
2020 |
Número de páginas: |
XXVI, 239 p. 73 ilustraciones, 35 ilustraciones en color. |
ISBN/ISSN/DL: |
978-3-030-63618-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: |
Ciencias de la Computación IngenierÃa de software Lenguajes de programación (computadoras electrónicas) Computadoras Propósitos especiales Lógica informática y fundamentos de la programación. TeorÃa de la Computación Lenguaje de programación Sistemas de propósito especial y basados ​​en aplicaciones |
Clasificación: |
40.151 |
Resumen: |
Este libro constituye las actas arbitradas de la 12.ª Conferencia Internacional sobre Software Verificado, VSTTE 2020, y el 13.º Taller Internacional sobre Verificación de Software Numérico, NSV 2020, celebrados en Los Ãngeles, CA, EE. UU., en julio de 2020. Debido a la pandemia de COVID-19 la conferencia se llevó a cabo virtualmente. Los 13 artÃculos presentados en este volumen fueron cuidadosamente revisados ​​y seleccionados entre 21 presentaciones. Los artÃculos describen esfuerzos de verificación a gran escala que involucran colaboración, unificación de teorÃas, integración de herramientas y conocimiento de dominio formalizado, asà como experimentos novedosos y estudios de casos que evalúan técnicas y tecnologÃas de verificación. La conferencia tuvo lugar junto con la 32.ª Conferencia Internacional sobre Verificación Asistida por Computadora (CAV 2020). |
Nota de contenido: |
SARL: OO Framework Specification for Static Analysis -- QPR Verify: A Static Analysis Tool for Embedded Software based on Bounded Model Checking -- Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX -- Automatic Detection and Repair of Transition-Based Leakage in Software Binaries -- BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers -- Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison -- Verfied Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language -- MCBAT: Model Counting for Constraints over Bounded Integer Arrays -- Optimized NTT Algorithm -- Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results? -- An Efficient Floating-Point Bit-Blasting API for Verifying C Programs -- Rigorous Enclosure of Round-O Errors in Floating-Point Computations : Towards Numerical Assistants: Trust, Measurement, Community, and Generality for the Numerical Workbench -- Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants -- SARL: OO Framework Speci cation for Static Analysis -- QPR Verify: A Static Analysis Tool for Embedded Software based on Bounded Model Checking -- Veri ed Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX -- Automatic Detection and Repair of Transition-Based Leakage in Software Binaries -- BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers -- Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison -- Veri ed Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language -- MCBAT: Model Counting for Constraints over Bounded Integer Arrays -- Verification of an Optimized NTT Algorithm -- Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results? -- An Efficient Floating-Point Bit-Blasting API for Verifying C Programs -- Rigorous Enclosure of Round-O Errors in Floating-Point Computations -- Towards Numerical Assistants: Trust, Measurement, Community, and Generality for the Numerical Workbench -- Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants. |
Tipo de medio : |
Computadora |
Summary : |
This book constitutes the refereed proceedings of the 12th International Conference on Verified Software, VSTTE 2020, and the 13th International Workshop on Numerical Software Verification, NSV 2020, held in Los Angeles, CA, USA, in July 2020. Due to COVID-19 pandemic the conference was held virtually. The 13 papers presented in this volume were carefully reviewed and selected from 21 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies. The conference was co-located with the 32nd International Conference on Computer-Aided Verification (CAV 2020). |
Enlace de acceso : |
https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] |
12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20–21, 2020, Revised Selected Papers [documento electrónico] / Christakis, Maria, ; Polikarpova, Nadia, ; Duggirala, Parasara Sridhar, ; Schrammel, Peter, . - 1 ed. . - [s.l.] : Springer, 2020 . - XXVI, 239 p. 73 ilustraciones, 35 ilustraciones en color. ISBN : 978-3-030-63618-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: |
Ciencias de la Computación IngenierÃa de software Lenguajes de programación (computadoras electrónicas) Computadoras Propósitos especiales Lógica informática y fundamentos de la programación. TeorÃa de la Computación Lenguaje de programación Sistemas de propósito especial y basados ​​en aplicaciones |
Clasificación: |
40.151 |
Resumen: |
Este libro constituye las actas arbitradas de la 12.ª Conferencia Internacional sobre Software Verificado, VSTTE 2020, y el 13.º Taller Internacional sobre Verificación de Software Numérico, NSV 2020, celebrados en Los Ãngeles, CA, EE. UU., en julio de 2020. Debido a la pandemia de COVID-19 la conferencia se llevó a cabo virtualmente. Los 13 artÃculos presentados en este volumen fueron cuidadosamente revisados ​​y seleccionados entre 21 presentaciones. Los artÃculos describen esfuerzos de verificación a gran escala que involucran colaboración, unificación de teorÃas, integración de herramientas y conocimiento de dominio formalizado, asà como experimentos novedosos y estudios de casos que evalúan técnicas y tecnologÃas de verificación. La conferencia tuvo lugar junto con la 32.ª Conferencia Internacional sobre Verificación Asistida por Computadora (CAV 2020). |
Nota de contenido: |
SARL: OO Framework Specification for Static Analysis -- QPR Verify: A Static Analysis Tool for Embedded Software based on Bounded Model Checking -- Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX -- Automatic Detection and Repair of Transition-Based Leakage in Software Binaries -- BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers -- Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison -- Verfied Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language -- MCBAT: Model Counting for Constraints over Bounded Integer Arrays -- Optimized NTT Algorithm -- Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results? -- An Efficient Floating-Point Bit-Blasting API for Verifying C Programs -- Rigorous Enclosure of Round-O Errors in Floating-Point Computations : Towards Numerical Assistants: Trust, Measurement, Community, and Generality for the Numerical Workbench -- Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants -- SARL: OO Framework Speci cation for Static Analysis -- QPR Verify: A Static Analysis Tool for Embedded Software based on Bounded Model Checking -- Veri ed Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX -- Automatic Detection and Repair of Transition-Based Leakage in Software Binaries -- BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers -- Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison -- Veri ed Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language -- MCBAT: Model Counting for Constraints over Bounded Integer Arrays -- Verification of an Optimized NTT Algorithm -- Can We Avoid Rounding-Error Estimation in HPC Codes and Still Get Trustworthy Results? -- An Efficient Floating-Point Bit-Blasting API for Verifying C Programs -- Rigorous Enclosure of Round-O Errors in Floating-Point Computations -- Towards Numerical Assistants: Trust, Measurement, Community, and Generality for the Numerical Workbench -- Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants. |
Tipo de medio : |
Computadora |
Summary : |
This book constitutes the refereed proceedings of the 12th International Conference on Verified Software, VSTTE 2020, and the 13th International Workshop on Numerical Software Verification, NSV 2020, held in Los Angeles, CA, USA, in July 2020. Due to COVID-19 pandemic the conference was held virtually. The 13 papers presented in this volume were carefully reviewed and selected from 21 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies. The conference was co-located with the 32nd International Conference on Computer-Aided Verification (CAV 2020). |
Enlace de acceso : |
https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] |
|  |