Content 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.
Scalable SPARK Proofs
This blog post explains how a SPARK function for counting character occurrences was formally verified to ensure both absence of runtime errors and…
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,…
Taking on a Challenge in SPARK
Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
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…
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…
Testing, Static Analysis, and Formal Verification
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…
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.
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.
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…
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…