Description

DIADEM -- A Deductive verIfication frAmework for higher-orDEr prograMs -- proposes a new methodology for the deductive verification of stateful code. We intend to explore the technique of defunctionalization, since it allows us to translate an higher-order program into a first-order equivalent counterpart. The resulting first-order program can then be fed into off-the-shelf automatic program verification tools.

It is funded by NOVA LINCS via a Target Research Activity project.