--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on April 2009 ---
>By the way, aren't Binary Decision Diagrams used in Frama-C? It is natural to think that they could, because value analysis with separation of states feels very much like "symbolic model checking" where the "model" is the C program being analyzed. In particular, if the C program happened to be a simulation, using boolean variables, of some kind of logic circuit, the value analysis (with separation of states) of the program would be equivalent to model-checking the circuit. But actual C programs do not have just boolean variables or variables whose values can conveniently be encoded in tuples of booleans, so the value analysis borrows ideas and algorithms from model-checking without literally relying on BDDs. And truth be told, "hash-consing" was invented in functional programming before being popularized with BDDs, so it's only fair to borrow it back. Pascal