Abstract
We present an enhancement of the generic fixpoint algorithm TD which can deal with widening and narrowing even for non-monotonic systems of equations. In contrast to corresponding enhancements proposed for other standard fixpoint algorithms, no extra priorities on variables are required. Still, a mechanism can be devised so that occurrences of the widening/narrowing operator are inserted as well as removed dynamically.
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
References
Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 25–42. Springer, Heidelberg (2013)
Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing (2015). arXiv:1503.00883 [cs.PL]
Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a Swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 157–172. Springer, Heidelberg (2012)
Apinis, K.: Frameworks for analyzing multi-threaded C, Ph.D. thesis, Institut für Informatik, Technische Universität München (2014)
Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 377–386. ACM (2013)
Bourdoncle, F.: Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In: Deransart, P., Małuszyński, J. (eds.) PLILP 1990. LNCS, vol. 456. Springer, Heidelberg (1990)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Robinet, B. (ed.) 2nd International Symposium on Programming, Paris, pp. 106–130. Dunod (1976)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM Press (1977)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conference on Formal Description of Programming Concepts, pp. 237–277. North-Holland (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) 6th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 269–282 (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 84–96. ACM Press (1978)
Fecht, C., Seidl, H.: Propagating differences: an efficient new fixpoint algorithm for distributive constraint systems. Nord. J. Comput. 5(4), 304–329 (1998)
Fecht, C., Seidl, H.: A faster solver for general systems of equations. Sci. Comput. Program. 35(2), 137–161 (1999)
Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 22(2), 187–223 (2000)
Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao System preprocessor). Sci. Comput. Program. 58(1), 115–140 (2005)
Hofmann, M., Karbyshev, A., Seidl, H.: Verifying a local generic solver in Coq. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 340–355. Springer, Heidelberg (2010)
Hofmann, M., Karbyshev, A., Seidl, H.: What is a pure functional? In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 199–210. Springer, Heidelberg (2010)
Kildall, G.A.: A unified approach to global program optimization. In: ACM Symposium on Principle of Programming Languages (POPL), pp. 194–206. ACM (1973)
Le Charlier, B., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Technical report 92–22, Institute of Computer Science, University of Namur, Belgium (1992)
Miné, A.: The octagon abstract domain. Higher-Order Symb. Comput. 19(1), 31–100 (2006)
Muthukumar, K., Hermenegildo, M.: Deriving a fixpoint computation algorithm for top-down abstract interpretation of logic programs. Technical report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759 (1990)
Puebla, G., Hermenegildo, M.: Optimized algorithms for the incremental analysis of logic programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145. Springer, Heidelberg (1996)
Seidl, H., Fecht, C.: Interprocedural analyses: a comparison. J. Log. Program. 43(2), 123–156 (2000)
Vojdani, V.: Static data race analysis of heap-manipulating C programs, Ph.D. thesis, University of Tartu, (2010)
Acknowledgements
The research leading to these results has received funding from the ARTEMIS Joint Undertaking under grant agreement no 269335 and from the German Science Foundation (DFG). This work was funded by institutional research grant IUT2-1 from the Estonian Research Council.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Apinis, K., Seidl, H., Vojdani, V. (2016). Enhancing Top-Down Solving with Widening and Narrowing. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-27810-0_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27809-4
Online ISBN: 978-3-319-27810-0
eBook Packages: Computer ScienceComputer Science (R0)