Development Log

  • SPARK Pro
    Mar 31st, 2016

    Deterministic proof by default with no timeout
    GNATprove is now deterministic by default, so it does not use timeouts unless explicitly instructed by the user to do so. Instead, a steps limit is used to bound the effort made by automatic provers to find a proof. This new design is based on a few changes: the proof level (switch --level) is 0 by default, proof level sets a value of steps but no value of timeout, switch --timeout takes a new value "auto", in addition to a possible time in seconds. The semantics of --timeout=auto is that it adjusts to the value of the proof level.