Abstract
Linear relation analysis [CH78, Hal79] 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.
This work was supported by the Department of the Navy, Office of the Chief of Naval Research under Grant N00014-91-J-1901, and by a grant from the Stanford Office of Technology Licensing. This publication does not necessarily reflect the position or the policy of the U.S. Government and no official endorsement of this work should be inferred.
This work was performed while the author was on leave in Stanford University.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, and D. Dill. Model checking of real-time systems. In Fifth IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.
R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems (extended abstract). In CONCUR'92, Stony Brook. LNCS 630, Springer Verlag, August 1992.
R. Alur. Techniques for automatic verification of real-time systems. Phd thesis, Stanford University, August 1991.
F. Boussinot and R. de Simone. The Esterel language. Proceedings of the IEEE, 79(9):1293–1304, September 1991.
P. Cousot and R. Cousot Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, January 1977.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Research Report LIX/RR/92/08, Ecole Polytechnique, March 1992. (to appear in the Journal of Logic Programming, special issue on Abstract Interpretation).
P. Cousot and R. Cousot. Comparing the Galois connection and widenning/narrowing approaches to abstract interpretation. Research Report UX/RR/92/09, Ecole Polytechnique, June 1992.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on Principles of Programming Languages, Tucson (Arizona), January 1978.
N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.
J. C. Corbett. Verifying general safety and liveness properties with integer programming. In G. Bochmann, editor, 4th Int. Workshop on Computer Aided Verification, Montreal, 1992.
D. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In 1991 IEEE Int. Conference on Computer Design: VLSIin Computers and Processors, 1992.
S. Devadas, K. Kreutzer, and A. S. Krishnakumar. Design verification ansd reachability analysis using algebraic manipulation. In ICCD'91, 1991.
N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Thèse de 3e cycle. University of Grenoble, March 1979.
N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6/7), 1992.
Another look at real-time programming. Special Section of the Proceedings of the IEEE, 79(9):1293–1304, September 1991.
M. Jourdan, F. Maraninchi, and A. Olivero. Verifying quantitative real-time properties of synchronous programs. In Fifth Int. Workshop on Computer Aided Verification, Elounda (Crete), July 1993.
H. LeVerge. A note on Chernikova's algorithm. Research Report 635, IRISA, February 1992.
E. Macii, B. Plessier, and F. Somenzi. Verification of systems containing counters. In ICCAD'92, 1992.
J. A. Plaice and J-B. Saint. The Lustre-Esterel portable format. Unpublished Report, INRIA, Sophia Antipolis, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Halbwachs, N. (1993). Delay analysis in synchronous programs. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_28
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive