Development Log

  • SPARK Pro
    Mar 21st, 2016

    Reproducible generation of VCs
    Previously, proof oblications (or VCs) generated by SPARK could be slightly different from one run of SPARK tools to the other. Now, if the source files have not changed, exactly the same VCs will be generated. This is useful if external tools are used to track or cache such VCs.