Very impressive work. Formal verification is slowly becoming real. A step forward for the field. Recently talked to the author, there is more to come. The magi

Very impressive work. Formal verification is slowly becoming real. A step forward for the field. Recently talked to the author, there is more to come. The magical essence: "As in our previous work [21], we use Dafny [39], a highlevel language that automates verification via the Z3 [11] SMT solver. This enables it to fill in many low-level proofs automatically; for example, it easily verifies the program in Figure 2 for all possible inputs x without any assistance." [39] http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ SMT solver = SAT solver, http://cvc4.cs.nyu.edu/web/ http://cvc4.cs.nyu.edu/web/