Muhammad Taimoor Khan,
"Translation of MiniMaple to Why3ML"
, Serie RISC Report Series, Nummer 13-01, RISC Hagenberg, Hagenberg, 2-2013
Original Titel:
Translation of MiniMaple to Why3ML
Sprache des Titels:
Englisch
Original Kurzfassung:
In this paper, we give the complete definition of the translation of MiniMaple and its specification language to an
intermediate language Why3ML of verification calculus Why3. For the verification, we first translate MiniMaple annotated program into a semantically equivalent
Why3ML program, then verification conditions are generated by using Why3 corresponding verification conditions generator. Finally, the correctness of the
generated verification conditions can be proved by various Why3 back-end supported automatic and interactive theorem provers.
Forschungs-