Last month I attended part of the Formal Methods Week 2009 in Eindhoven. Each year the FMWeek brings the world of formal verification together, with an emphasis on academic and industrial partnerships.
Although I am familiar with the field, I was still impressed by what is currently possible with tools based on formal methods. Although it will never be 100% automated, you can already get very strong guarantees on industrial products with high levels of automation.
Two examples show it better:
Airbus presented their use of formal verification tools for DO-178B software. Five of the six tools that were presented are in use within operational units. This presentation echoed, 10 years later, the presentation they gave at FM 1999 about their first trial with formal verification. With a decade of experience in industrial use of such tools, they have defined 5 “must-have” criteria: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improve on classical methods, certifiability. Very important lessons indeed.
André Platzer from CMU presented his work on formal verification of flight collision avoidance maneuvers which won the best paper award. This is quite a leap in coverage of formal methods: verifying nonlinear properties involving curves, differential equations etc. with almost complete automation.
Just to give you a flavor of it:
