Wiki Agenda Contact Version française

Double WP

This is a case study formalizing a toy compiler and proving its correctness. There are two versions given below. The first version is presented in the paper Double WP: vers une preuve automatique d'un compilateur and is compatible with Why3 0.88. The second version is adapted to the future major release of Why3 (currently available as the 'new_system' branch of the git repository). This second version makes use of type invariants.

Authors: Léon Gondelman / Martin Clochard

Topics: Semantics of languages

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

The version compatible with Why3 0.88 is described there.

download ZIP archive

The version compatible with the new Why3 system is described there.

download ZIP archive