Re:IronFleet: Proving Practical Distributed Systems Correct ...
by synctext on Monday October 19, 2015 @04:42AM
(#10411806)
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."
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/