SYRF Project

Task 3.4: "Deductive Proofs of Data-flow Programs"

Abstract of deliverable 3.4.2

Back to the SYRF Home Page



Approach:

This task aims at providing methods and tools for applying deductive tools to synchronous programs that cannot be model-checked. As examples, the chosen synchronous language is Lustre and the deductive proof tool is PVS.

Achieved Results: We reworked the translation tool from Lustre to PVS made unavailable because of evolutions in PVS. We propose a translation method apparently more robust with respect to such evolutions and which seems to correct most drawbacks of the previous one:

Conclusion: Though not yet fully evaluated, this method looks quite appealing and we propose to prototype it in the coming year.