About synchronous programming and abstract interpretation

Abstract:
This paper intends to highlight the connection between synchronous programming and abstract interpretation. First, the specific technique for compiling synchronous programs into interpreted automata can be seen as a partial evaluation. The second point concerns program verification. Most critical properties of reactive systems are safety properties, which can be translated into invariants, through the use of {\em synchronous observers}. Invariants can be proved by means of approximate reachability analysis, which is probably the most studied application of abstract interpretation.

Reference:

@INPROCEEDINGS{halbwachs94c,
   AUTHOR={N. Halbwachs},
   TITLE={About synchronous programming and abstract interpretation},
   BOOKTITLE={International Symposium on Static Analysis, SAS'94},
   EDITOR = {B. {LeCharlier}},
   PUBLISHER = {LNCS 864, Springer Verlag},
   ADDRESS = {Namur (belgium)},
   MONTH = {September},
   YEAR= 1994
}

Extended verion published in journal={Science of Computer Programming,Special Issue on SAS'94}, editor={P. Cousot and B. Le Charlier}, volume= 31, number= 1, month= {May}, year=1998

Postscript file