1. 4

  2. 3

    Leon is a verification tool for a subset of Scala that can “repair contracts, fix erroneous implementations, and even synthesize implementations.” GenC converts that Scala subset to a safety-critical subset of C99 to leverage C compilers and run on embedded systems. The goal is to get Scala’s productivity, partial verification of the software, and release code in C without its safety problems.


    Past that, I have no idea as the site for Leon is down and once again not in Wayback. (sighs) I emailed the author about that.