Blog Posts by Roderick Chapman
Roderick Chapman
Protean Code Limited
Rod is Director of Protean Code Limited. He specializes in the design, implementation and verification of high-integrity software systems. For many years, Rod led the SPARK design team at Praxis and Altran in the UK, and continues to work closely with the SPARK team at AdaCore.
Roderick Chapman
SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance
This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at…
Roderick Chapman
Doubling the Performance of SPARKNaCl (again...)
Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack…
Roderick Chapman
Performance analysis and tuning of SPARKNaCl
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and…
Roderick Chapman
Proving properties of constant-time crypto code in SPARKNaCl
Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under…
Yannick Moy, Roderick Chapman
How Ada and SPARK Can Increase the Security of Your Software
There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the…