For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle. The triangle captures a trade-off between three desirable properties: Automation – the verification tool runs largely without human guidance Scalability – the technique works on large real systems Precision – the method can prove interesting properties, such as functional correctness Historically, verification techniques could reliably achieve two of the three, but not all three simultaneously.
No pages have linked to this URL yet.