After the general presentation of formal verification of programs and circuits in the 2014-2015 lecture, the 2015-2016 lecture was devoted to automatic verification methods based on decidable theories. These methods, some of which were introduced as early as the 1960s, have made considerable progress in recent years with the invention of new, remarkably efficient algorithms and the combination of these algorithms. They have the advantage of requiring little knowledge of their inner workings on the part of the user, who can therefore devote more time to his or her own problem. They are widely used industrially in the world of electronic circuits, either to verify behavior, or to validate the many processing stages from specification to final circuit mask. In software, they are increasingly used as the ideal complement to type systems for detecting errors as early as compilation, for static analysis bug-finding, and for automatic generation of directed tests.
The lecture looked at the main automatic methods and their applications:
- first, binary decision diagrams (BDDs), the first efficient Boolean computation structure already briefly presented and used in previous lectures;
- secondly, algorithms for analyzing the satisfiability of large Boolean formulas, the so-called SAT problem. These have made enormous progress over the last twenty years and have become standard tools in many fields of computer science, and SMT (satisfiability modulo theories) algorithms, which can verify much richer arithmetic or symbolic formulas;
- secondly, verification algorithms for timed automata, adapted to the validation of real-time systems;
- finally, explicit algorithms, which enumerate the states and transitions of a system rather than treating it symbolically.