This paper is a must-read if you want to bring formal methods to industry.
Continuous Reasoning: Scaling the impact of formal methods
by Peter W. O’Hearn, Facebook and University College London
dl.acm.org/citation.cfm?i…
Continuous Reasoning: Scaling the impact of formal methods
by Peter W. O’Hearn, Facebook and University College London
dl.acm.org/citation.cfm?i…
If you're familiar with formal methods, some of this will be very comfortable.
Composition is important, and it's better if it is automated.
Low false positive rate (for bugs found) is a big deal.
Composition is important, and it's better if it is automated.
Low false positive rate (for bugs found) is a big deal.
The tool briefly describes Infer, a tool pulled out of Academia and invested in heavily at Facebook, in order to make it a push-button tool for a wide range of projects (this tweet is my take on Infer, not from the paper)
Here's the staggering fact about Infer application.
At first they sent bugs out each night... Nobody fixed anything. They moved the analysis to commit/push time and fixes topped 70%.
This is in the paragraph titled "The ROFL Episode". The paper goes on to explain why.
At first they sent bugs out each night... Nobody fixed anything. They moved the analysis to commit/push time and fixes topped 70%.
This is in the paragraph titled "The ROFL Episode". The paper goes on to explain why.
I want to put this in front of some motivational scenery and frame it.
Tens. Of. Thousands.
Tens. Of. Thousands.
The paper then cites some pretty great work
VST (I worked on this at Princeton) and Dafny are proofs tools that use "manual compositionality". This is another way of saying they require hand-written specs, while tools like Infer require none "automatic compositionality"
VST (I worked on this at Princeton) and Dafny are proofs tools that use "manual compositionality". This is another way of saying they require hand-written specs, while tools like Infer require none "automatic compositionality"
Then our (@galois) work with Amazon gets a half-page. I've written enough about that, but I'll share a chart from the paper giving a concise summary of the difference between our proofs and Infer proofs.
There are few more references including a very positive (and well deserved) summary of SPARK, which is commonly used for safety-critical software.
adacore.com/about-spark
adacore.com/about-spark
Infer often works on partial code, with partial information, so the question of when it should raise an alarm for a problem is a complicated one. The paper gives good insight into this.
There's a lot more to the paper, hopefully these tweets piqued your interest so you go check it out. The information density is perfect for a straight read through, which I find to be rare thing from academic papers. If nothing else, check out the conclusion. It stands alone.
