Development Log

  • SPARK Pro
    Mar 20th, 2017

    Theories for conversion of discrete types realized
    The Why3 theories used by GNATprove to model conversions between discrete types have been realized in Coq. This increases confidence in their correction.