![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > A Verified Bignum Implementation in x86-64 Machine Code
A Verified Bignum Implementation in x86-64 Machine CodeAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact William Denman. This is a 20-minute preview of a talk I’ll give at CPP ’13. Verification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessitate ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using an abstraction for arrays and previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover. The case study resulted in 800 lines of verified 64-bit x86 machine code. This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsSeminars on Adaptation to Climate Change Market Square – The Cambridge Business & Society Interdisciplinary Research Group CU Pakistan SocietyOther talks"Itsa me! Luigi!" [citation needed] - unlocking your referencing skills Holonomic D-modules, b-functions, and coadmissibility Rather more than Thirty-Nine Steps: the life of John Buchan Hide and seek: medieval creatures on the manuscript page Computer vision techniques for measuring deformation Panel Discussion: Climate Change Is Now |