Johannes Kanig - Personal Website

I am now devoting much of my time at work to the Hi-Lite project. This is a quite ambitious project, which brings program verification to the Ada programming language. The programmer has to write contracts for his program functions; these executable contracts are simply Ada expressions, more precisely Ada 2012 expressions, which allow the expression of complex properties more easily. These contracts can then be exploited either for conventional unit testing, where contracts act as additional assertions, or for more advanced unit proving, where the correctness of a program function, and the absence of runtime errors is proven using the state-of-the-art VC generator Why3 (see below) and SMT prover Alt-ergo.

When I encountered the problem of creating figures for documents created with LaTeX, I quickly began to use Metapost, which is one of the few solutions to provide a good integration of LaTeX snippets in the figure, and a good integration of the figure into the LaTeX document. Also, Metapost allows to program a figure, which enables parametric figures, libraries for often-used forms and so on. Unfortunately, Metapost is a very poor programming language, so that any more advanced development is impossible (I am not saying that complex figures are not possible, but complex programs with complex datastructures are nearly impossible in pure metapost).

With my collegues at LRI, we therefore came up with Mlpost, an OCaml library quite similar to Metapost in principle, i.e., building figures using programs, with the possibility to include LaTeX snippets, and easy integration of the resulting figure into LaTeX documents. But this library is embedded in a powerful general purpose programming language, which allows figures to be the result of the run of a complex algorithm, and allows powerful datastructures such as trees to be easily integrated into figures.

Mlpost started as a simple pretty printer for Metapost, but has grown into an alternative implementation of some of the algorithms in Metapost; the recommended backend for the actual creation of figures is now the Cairo backend.

The verification generator Who for imperative programs with higher-order functions is a proof-of-concept implementation of the theory developed in my PhD thesis (see the research section). It should now be considered a dead project, as I don't have time to develop on it anymore. Hopefully, most of the functionality of Who will find its way into Why3 one day. The source code is still available; a prerequisite is the usage of Ocaml 3.11.2.

Why3 is a verification condition generator. What that means is that it takes a program, with annotations such as contracts, loop invariants or assertions, and generates verification conditions, i.e., formulas which, when proven, imply the correctness of the program. Why3 is a powerful programming language, logical specification language and a well-desiged tool, and it is more than a simple VCgen. It supports a variety of provers, can call provers automatically, with timeout management and parallelism, and a graphical interface to write and prove programs.

I cannot honestly call myself a Why3 developer, but I am a huge fan of the project and I participated a bit in the initial core design of the tool and the language during my time at LRI.