Verifying branch-free assembly code in Why3

DOI10.1007/978-3-319-72308-2_5zbMath1403.68027OpenAlexW2773698228MaRDI QIDQ1630029

Marc Schoolderman

Publication date: 7 December 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-72308-2_5

zbMATH Keywords

assembly languageWhy3Karatsuba multiplication

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (3)

WhyMP, a formally verified arbitrary-precision integer library ⋮ Deductive Binary Code Verification Against Source-Code-Level Specifications ⋮ Unnamed Item

Uses Software

• Why3

This page was built for publication: Verifying branch-free assembly code in Why3