Blog Posts by Johannes Kanig
Johannes Kanig
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.
Joffrey Huguet, Johannes Kanig
Proving a simple program doing I/O ... with SPARK
The functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip,…
Johannes Kanig
Taking on a Challenge in SPARK
Johannes Kanig
Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
Johannes Kanig
Hash it and Cache it
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…
Johannes Kanig
SPARK and CodePeer, a Good Match!
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…
Johannes Kanig
Testing, Static Analysis, and Formal Verification
Johannes Kanig
SPARK 15: Errors, Warnings and Checks
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…
Johannes Kanig
Explicit Assumptions in SPARK 2014
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
Johannes Kanig
Prove in Parallel with SPARK 2014
The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.
Johannes Kanig
A Little Exercise With Strings
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…
Johannes Kanig
SPARK 2014 goes to Space!
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…