author = {Muhammad Taimoor Khan},
title = {{Translation of MiniMaple to Why3ML}},
language = {english},
abstract = {In this paper, we give the complete definition of the translation of MiniMaple and its specification language to an intermediate language Why3ML of verification calculus Why3. For the verification, we first translate MiniMaple annotated program into a semantically equivalent Why3ML program, then verification conditions are generated by using Why3 corresponding verification conditions generator. Finally, the correctness of the generated verification conditions can be proved by various Why3 back-end supported automatic and interactive theorem provers},
number = {13-01},
year = {2013},
month = {February},
sponsor = {FWF},
length = {58},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}