Abstract
We employ static analysis to examine monotonicity of functions defined over lattices in a λ-calculus augmented with constants, branching, meets, joins and recursive definitions. The need for such a verification procedure has recently arisen in our work on a static analyzer generator called Zoo, in which the specification of static analysis (input to Zoo) consists of finite-height lattice definitions and function definitions over the lattices. Once monotonicity of the functions is ascertained, the generated analyzer is guaranteed to terminate.
This work is supported by Creative Research Initiatives of the Korean Ministry of Science and Technology.
On leave from Nicholas Copernicus University, Toruń, Poland.
ROPAS - Research On Program Analysis System (http://ropas.kaist.ac.kr), National Creative Research Initiative Center, KAIST, Korea.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238–252, 1977.
Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Journal of Logic Computation, 2(4):511–547, 1992. Also as a tech report: Ecole Polytechnique, no. LIX/RR/92/10.
Patrick Cousot and Radhia Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Lecture Notes in Computer Science, volume 939, pages 293–308. Springer-Verlag, proceedings of the 7th international conference on computer-aided verification edition, 1995.
Yevgeniy Dodis, Oded Goldreich, Eric Lehman, Sofya Raskhodnikova, Dana Ron, and Alex Samorodnitsky. Improved testing algorithms for monotonicity. Number Report TR99-107 in Electronic Colloquium on Computational Compleity, June 1999.
Oded Goldreich, Shafi Goldwasser, Eric Lehman, and Dand Ron. Testing monotonicity. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science, 1998.
B. Le Charlier and P. Van Hentenryck. A universal top-down fixpoint algorithm. Technical Report TR-CS-92-25, Brown University, Dept. of Computer Science, May 1992. (also as a technical report of Institute of Computer Science, University of Namur).
B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. ACM Transactions on Programming Languages and Systems, 16(1):35–101, January 1994.
Florian Martin. PAG — an efficient program analyzer generator. International Journal on Software Tools for Technology Transfer, 2(1):46–67, 1998.
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.
D.E. Rutherford. Introduction to Lattice Theory. Hafner Publishing Company, New York, 1965.
Winfrid G. Schneeweiss. A necessary and sufficient criterion for the monotonicity of boolean functions with deterministic and stochastic. IEEE Transactions on Computers, 45(11):1300–1302, November 1996.
Jean-Pierre Talpin and Pierre Jouvelot. Type, effect and region reconstruction in polymorphic functional languages. In Proceedings of Functional Programming Languages and Computer Architecture, 1991.
Jean-Piere Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, July 1992.
Mads Tofte and Jean-Pierre Talpin. A theory of stack allocation in polymorphically typed languages. Technical Report Technical Report 93/15, Department of Computer Science, Copenhagen University, July 1993.
Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call by-value λ-calculus using a stack of regions. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188–201, January 1994.
Andrei Voronenko. On the complexity of the monotonicity verification. In Proceedings of the 15th Annual IEEE Conference on Computational Complexity, pages 4–7, July 2000.
Kwangkeun Yi and Williams Ludwell Harrison III. Automatic generation and management of interprocedural program analyses. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 246–259, January 1993.
Kwangkeun Yi. Program Analysis System Zoo. Research On Program Analysis: National Creative Research Center, KAIST, July 2001. http://ropas.kaist.ac.kr/zoo/doc/rabbit-e.ps.
Kwangkeun Yi. System Zoo: towards a realistic program analyzer generator, July 2001. Seminar talk at ENS, Paris. http://ropas.kaist.ac.kr/~kwang/talk/ens01/ens01.ps.
Kwangkeun Yi and Sukyoung Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Proceedings of the 4th International Static Analysis Symposium, volume 1302 of Lecture Notes in Computer Science, pages 98–113. Springer-Verlag, 1997.
Kwangkeun Yi and Sukyoung Ryu. A cost-effective estimation of uncaught exceptions in Standard ML programs. Theoretical Computer Science, 273(1), 2001. (to appear).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murawski, A.S., Yi, K. (2002). Static Monotonicity Analysis for λ-definable Functions over Lattices. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_10
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive