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/

SMT solver = SAT solver, http://cvc4.cs.nyu.edu/web/

There's a blog post discussing the paper available at http://blog.acolyer.org/2015/10/15/ironfleet-proving-practic...