| 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. |
| 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 |
| Ãndice Dewey: |
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. |
| 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 |
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.
| 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 |
| Ãndice Dewey: |
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. |
| 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 |
|  |