Johannes Kanig is a senior software engineer at AdaCore and developer of the SPARK technology. He received his PhD in formal verification from the University Paris-Sud, France.
10 entries written by Johannes Kanig
Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.
Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!
A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on different machines. Check out this post to see the details.
It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!
I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).
The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the motivation behind it.
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.
I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function and it's proof are quite simple in the end, the process of obtaining the correct code and the proof was interesting enough to write this blog post.
David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried GNATprove - the formal verification tool for SPARK 2014 - on space vehicle software as an industrial case study of the project. And it turns out GNATprove performed pretty well!