--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] The Capabilities of Frama-C



>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