Johannes Kanig - Personal Website

Cyrille Comar, Johannes Kanig and Yannick Moy (all AdaCore).

ERTS 2012, Toulouse, Feb. 2012

Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as DO-178C for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study.

[pdf]

Jérôme Guitton, Johannes Kanig and Yannick Moy (all AdaCore).

Boogie Workshop, Wroclaw, August 2011.

Use of formal methods in verification activities for critical software development is a promising solution to increase the level of confidence compared to the current practice based on testing, for increasingly complex programs, at a lower cost than the current approach. Concretely, the upcoming standard DO-178C for software development in avionics gives credit to formal verification for supporting verification activities. In project Hi-Lite, we pursue the integration of formal proofs with unit testing, for selected parts of a larger C or Ada software development. This integration relies crucially on a common language of specification between testing and formal proofs, where both share the same assertion semantics. For Ada, this language of specification based on subprogram contracts is part of the upcoming standardized version Ada 2012 of the language. In this paper, we describe the specifics of our translation from Ada to the intermediate verification language Why, noting which features of Why we used in our translation, and from which extensions of Why we could benefit in the future.

[pdf]

Johannes Kanig, Jérôme Guitton and Yannick Moy (all AdaCore).

Workshop Ada Deutschland, Stuttgart, June 2011.

Formal methods and testing are often considered as disjoint technologies. The Hi-Lite project wants to show that both are actually complementary. The central concept are subprogram contracts, part of the upcoming Ada 2012 standard. A contract, which consists of pre- and postcondition, describes the specification of a subprogram, in the same syntax as Ada expressions. These contracts can be seen either as additional assertions in the case of testing, or they can be used to prove the correctness of the subprogram, using modern proof technology such as SMT solvers. This mechanism allows an easy adoption of modern formal methods, on a per-function basis. Hi-Lite fits in well with the upcoming DO-178C avionics safety standard, a revision to DO-178B, which, among other things, accounts for technologies such as formal methods.

A contract is additional information a programmer has to write, and errors are possible. Another focus of the Hi-Lite project is to help the programmer write meaningful and complete contracts. Current proposals include the detection of runtime errors contained in contracts, meaningless or too strong contracts, incomplete contracts that do not mention modified variables and code that does not contribute to the contract.

The goal of project Hi-Lite is to produce a verification toolchain combining formal methods and testing, integrated with the usual project structure in the two IDEs developed by AdaCore.

[pdf]

Johannes Kanig.

Université Paris-Sud 11, Orsay, France, 2010.

In this thesis, we first present a theoretical system that enables proof of higher-order programs with side effects. This system consists of three major parts. First, a programming language with a traditional type, effect and region system, with effect polymorphism. Second, a higher-order specification language, that also contains a means to describe modifications of the state. Finally, a weakest precondition calculus that, starting from an annotated program, allows to obtain proof obligations, that is, formulas whose validity implies the correctness of the program w.r.t. its specification. We also present two restrictions of the initial system. The first disallows region aliasing, obtaining better modularity of the calculus, the second restricts the system to regions that are singleton, containing only a single reference. Both restrictions enable important simplifications that can be applied to proof obligations, but restrict the set of accepted programs.

We also present an implementation of this theoretical system, called Who. This tool uses in particular translations of the proof obligations to higher-order logic and first-order logic; these translations are detailed in this thesis. The translation to higher-order logic in particular allows using the Coq proof assistant to validate proof obligations. The translation to first-order logic allows using automated theorem provers. Higher-order programs, found in the standard library of OCaml and elsewhere, have been proved correct using the tool Who, as well as a continuation-based implementation of the Koda-Ruskey algorithm.

[pdf]

Johannes Kanig and Jean-Christophe Filliâtre.

In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009

We present Who, a tool for verifying effectful higher-order functions. It features Effect polymorphism, higher-order logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is intended to be used as an intermediate language for verification tools targeting ML-like programming languages.

[pdf]

Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig andStéphane Lescuyer.

In Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, January 2009

Cet article présente Mlpost, une bibliothèque Ocaml de dessin scientifique. Elle s'appuie sur metapost, qui permet notamment d'inclure des fragments LaTeX dans les figures. Ocaml offre une alternative séduisante aux langages de macros LaTeX, aux langages spécialisés ou même aux outils graphiques. En particulier, l'utilisateur de Mlpost bénéficie de toute l'expressivité d'Ocaml et de son typage statique. Enfin Mlpost propose un style déclaratif qui diffère de celui, souvent impératif, des outils existants.

[pdf]

Sylvain Conchon, Evelyne Contejean, Johannes Kanig and Stéphane Lescuyer.

In Electr. Notes Theor. Comput. Sci.198(2):51-69 2008

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantical values for class representatives instead of canonized terms. Using semantical values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

[pdf]

Sylvain Conchon, Johannes Kanig and Stéphane Lescuyer

In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, January 2008

Le problème SAT, qui consiste à déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en Ocaml d'un SAT-solver, baptisé SAT-Micro, intégrant ces optimisations ainsi qu'une mise en forme normale conjonctive paresseuse. Le fonctionnement de SAT-Micro est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.

[ps]

Sylvain Conchon, Evelyne Contejean, Johannes Kanig and Stéphane Lescuyer.

In AFM07 (Automated Formal Methods), Atlanta, Georgia, USA, November 2007

Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.

[pdf]

Sylvain Conchon, Evelyne Contejean and Johannes Kanig.

In 5th International Workshop on Satisfiability Modulo, Berlin, Germany, July 2007

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and a union X of solvable theories. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak approach by the use of semantical values for class representatives instead of syntactical canonizers. This seemingly insignificant difference has strong impact on efficiency and expressiveness. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

[ps]