RISC JKU
  • @techreport{RISC4678,
    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)}
    }