000 05661nam a22006135i 4500
001 978-3-030-63618-0
003 DE-He213
005 20240730174821.0
007 cr nn 008mamaa
008 201205s2020 sz | s |||| 0|eng d
020 _a9783030636180
_9978-3-030-63618-0
024 7 _a10.1007/978-3-030-63618-0
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aSoftware Verification
_h[electronic resource] :
_b12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers /
_cedited by Maria Christakis, Nadia Polikarpova, Parasara Sridhar Duggirala, Peter Schrammel.
250 _a1st ed. 2020.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2020.
300 _aXXVI, 239 p. 73 illus., 35 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aProgramming and Software Engineering,
_x2945-9168 ;
_v12549
505 0 _aSARL: 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.
520 _aThis 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).
650 0 _aComputer science.
_99832
650 0 _aSoftware engineering.
_94138
650 0 _aProgramming languages (Electronic computers).
_97503
650 0 _aComputers, Special purpose.
_946653
650 1 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aSoftware Engineering.
_94138
650 2 4 _aTheory of Computation.
_9114210
650 2 4 _aProgramming Language.
_939403
650 2 4 _aSpecial Purpose and Application-Based Systems.
_946654
700 1 _aChristakis, Maria.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9114211
700 1 _aPolikarpova, Nadia.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9114212
700 1 _aDuggirala, Parasara Sridhar.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9114213
700 1 _aSchrammel, Peter.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9114214
710 2 _aSpringerLink (Online service)
_9114215
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783030636173
776 0 8 _iPrinted edition:
_z9783030636197
830 0 _aProgramming and Software Engineering,
_x2945-9168 ;
_v12549
_9114216
856 4 0 _uhttps://doi.org/10.1007/978-3-030-63618-0
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c89638
_d89638