Delay analysis in synchronous programs

Abstract:
Linear relation analysis [Cousot&Halbwachs78] has been proposed a long time ago as an abstract interpretation which permits to discover linear relations invariantly satisfied by the variables of a program. Here, we propose to apply this general method to variables used to count delays in synchronous programs. The ``regular'' behavior of these counters makes the results of the analysis especially precise. These results can be applied to code optimization and to the verification of real-time properties of programs.

Reference:

   @INPROCEEDINGS{polys,
      AUTHOR={N. Halbwachs},
      TITLE={Delay analysis in synchronous programs},
      BOOKTITLE= {Fifth Conference on Computer-Aided Verification},
      ADDRESS={Elounda (Greece)},
      PUBLISHER = {LNCS 697, Springer Verlag},
      MONTH={July },
      YEAR=1993
   }

Postscript file