3 ms·
IronFleet: Proving Practical Distributed Systems Correct [pdf]
- synctext 11y agoVery 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/
- domsj 11y agoThere's a blog post discussing the paper available at http://blog.acolyer.org/2015/10/15/ironfleet-proving-practical-distributed-systems-correc/ http://blog.acolyer.org/2015/10/15/ironfleet-proving-practic...