[SystemSafety] Empirical Study on the Correctness of, Formally Verified Distributed Systems

[Derek M Jones]

José,

> As it reads, the quoted text might be a bit misleading. For the sake of
> completeness, I'd add a bit more of text extracted from the paper:

Yes, I let the snake oil salesmen in formal methods drag me
down to their level.

> On the positive side, still from the paper: "The absence of protocol bugs
> found in the verified systems sharply contrasts with the results of an
> analysis we conducted of known bugs in unverified distributed systems."

The comparison needs to be against systems verified using other
techniques.  Given X resources, which technique produces the most
reliable software?  Alternative, which technique can most cheaply
deliver reliability Y?

What does using "formal methods" actually mean?
http://shape-of-code.coding-guidelines.com/2016/08/29/does-using-formal-methods-mean-anything/

This paper provides an engineering view of using maths to
show properties:
https://alastairreid.github.io/papers/fmcad2016-trustworthy.pdf

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com