Combining Forward And Backward Analyses of Temporal Properties
- 160 Downloads
In this paper we extend the well-known combination of forward and backward static analyses in abstract interpretation for the verification of complex temporal properties for transition systems. First, we show that this combination, whose results are often better than those obtained by using both analyses separately, can be used to check simple temporal properties with just one fixpoint. Then we extend this result to more complex temporal properties, including a superset of Ctl in the case of non-game properties, and a superset of Atl in the case of game properties.
Unable to display preview. Download preview PDF.
- R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pages 100–109. IEEE Computer Society Press, 1997.Google Scholar
- F. Bourdoncle. Abstract debugging of higher-order imperative languages. In Proceedings of SIGPLAN’ 93 Conference on Programming Language Design and Implementation, pages 46–55, 1993.Google Scholar
- E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT press, 1999.Google Scholar
- P. Cousot. Méthodes itératives de construction et d’approximation de point fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. Thèse ès sciences mathématiques, University of Grenoble, March 1978.Google Scholar
- P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.Google Scholar
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.Google Scholar
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269–282, San Antonio, Texas, 1979. ACM Press, New York, NY.Google Scholar
- P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12–25, Boston, Mass., 2000. ACM Press, New York, NY.Google Scholar
- P. Granger. Improving the results of static analyses of programs by local decreasing iterations. In R. K. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, 12th conference, New Dehli, India, volume 652 of Lecture Notes in Computer Science, pages 68–79. Springer-Verlag, 1992.Google Scholar
- T.A. Henzinger, O. Kupferman, and S. Qadeer. From prehistoric to postmodern symbolic model checking. In A.J. Hu and M.Y. Vardi, editors, CAV 98: Computeraided Verification, volume 1427 of Lecture Notes in Computer Science, pages 195–206. Springer-Verlag, 1998.Google Scholar
- T.A. Henzinger, R. Majumdar, F.Y.C. Mang, and J.-F. Raskin. Abstract interpretation of game properties. In J. Palsberg, editor, SAS 00: Static Analysis, volume 1824 of Lecture Notes in Computer Science, pages 220–239. Springer-Verlag, 2000.Google Scholar