Abstract
The lecture will begin with an overview of the 2016 lectures on data structures and algorithms for formal verification. The scope of these lectures will be limited to automatic verification, mainly in decidable cases.
After a general presentation of the 2016 lectures, followed by a reminder of the main notions of algorithmic complexity and Boolean calculus, the lecture studied binary decision diagrams(BDDs). These were the first structures to revolutionize Boolean calculus, which is essential in many fields of application, but which was long thought to be unusable in practice due to its complexity: Boolean satisfaction is the prototype of the NP-complete problem.
BDDs were introduced by several authors in the 1970s, but systematized and put into practice thanks to the fundamental work of Randy Bryant at Carnegie-Mellon in the late 1980s. These are graphs with maximal sharing that realize a compact canonical form of Boolean expressions, modulo the given order of the variables appearing in these expressions. Canonicality implies that the equality of Boolean functions is decided in constant time, while logical operations are performed in polynomial time in a simple recursive fashion. We'll look at the efficient implementation of BDDs, then show the decisive influence of variable order on their size, as well as heuristics for avoiding their memory explosion as far as possible. Using examples linked to the Esterel language studied in previous years, we'll explain why BDDs are well suited to the synthesis, optimization and verification of complex circuits or controls in software programs. The following seminar will explore these issues in greater depth in the field of electronic circuits.
