Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code
No abstract available.
DOI 10.1007/978-3-319-03545-1_5
Related papers
- The verified CakeML compiler backend JFP 2019
- Verified just-in-time compiler on x86 POPL 2010
- Formally verified big step semantics out of x86-64 binaries CPP 2019
- Verified Cryptographic Code for Everybody CAV 2021
- Relaxing safely: verified on-the-fly garbage collection for x86-TSO PLDI 2015
- Modular development of certified program verifiers with a proof assistant ICFP 2006
- Modular development of certified program verifiers with a proof assistant, JFP 2008
- Verified compilation of CakeML to multiple machine-code targets CPP 2017