supervision by Jorge Sousa Pinto co-supervision by Lúıs Pinto

Supervisor’s signature: Co-supervisor’s signature: SPARK is a subset of the Ada programming language, extended with annotations, contracts and providing its own toolset, that has been suc-cessfully used in several industrial products for embedded and real-time programming of critical systems. Even though SPARK and its toolset have become very popular over these past few years, we find that the tool support for automatic and manual proving is rather limited. We also believe that there is little docu-mentation for these tools and that they have very particular characteristics which make them hard to learn and use effectively. In this thesis, we intend to improve upon SPARK essentially by for-malizing a meaningful subset of the language and creating for such subset a VCGen for a multi-prover target (e.g. Jessie) and thus allow proving, automatic and interactive, to be made with a wider collection of well known tools.