Verifying branch-free assembly code in Why3

DOI10.1007/978-3-319-72308-2_5MaRDI QIDQ1630029zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Modular verification of SPARCv8 code
• scientific article; zbMATH DE number 1670745
• scientific article; zbMATH DE number 7378548
• Verification of safety properties for concurrent assembly code
• Highly automated formal proofs over memory usage of assembly code

Cited in

(9)

• Modular verification of SPARCv8 code
• How to get an efficient yet verified arbitrary-precision integer library
• WhyMP, a formally verified arbitrary-precision integer library
• Deductive binary code verification against source-code-level specifications
• scientific article; zbMATH DE number 1670745 (Why is no real title available?)
• Highly automated formal proofs over memory usage of assembly code
• Low-level reachability analysis based on formal logic
• Verification of safety properties for concurrent assembly code
• A Why3 proof of GMP algorithms

Describes a project that uses

Uses Software

• Why3

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1630029)