Development Log

  • SPARK Pro
    Nov 22nd, 2016

    Better interval analysis of int to float conversions
    Interval analysis is a simple analysis that allows proving range checks and overflow checks simply by computing the worst-case bounds of expressions based on the types of subexpressions. This analysis now also deals precisely with conversions from integers to floating-point types, which improves provability of programs with such conversions.