SYRF Project

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

Abstract of deliverable 3.4.1

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:

Conclusion: The main lesson that can be drawn from this experiment is the following: we initially assumed that users wanted to stay as near as possible from their initial data-flow formalism. If this is true, both performed translations fail in the sense that, if a given property is not automatically proved, users have to deal with it in the PVS language and not in the source language. This leads us to think that the real problem is not the particular chosen translation method, but an inverse translation allowing prover sequents to be expressed in terms of the source language. We therefore propose to investigate this question in the coming year.

Publications:

  1. P. Caspi and M. Pouzet.
    A co-iterative characterization of synchronous stream functions.
    RR. nr. 97-07, Verimag, October 1997. Annex A.3.4.1a