Abstract
In the present paper we compute numerical invariants of programs by abstract interpretation. For that we consider the abstract domain of quadratic zones recently introduced by Adjé et al. [2]. We use a relaxed abstract semantics which is at least as precise as the relaxed abstract semantics of Adjé et al. [2]. For computing our relaxed abstract semantics, we present a practical strategy improvement algorithm for precisely computing least solutions of fixpoint equation systems, whose right-hand sides use order-concave operators and the maximum operator. These fixpoint equation systems strictly generalize the fixpoint equation systems considered by Gawlitza and Seidl [11].
This work was partially funded by the ANR project ASOPT.
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.
Similar content being viewed by others
References
Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.): ICALP 2008, Part I. LNCS, vol. 5125, pp. 973–978. Springer, Heidelberg (2008)
Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010) ISBN 978-3-642-11956-9
Björklund, H., Sandberg, S., Vorobyov, S.: Optimization on completely unimodal hypercubes. Technichal report 2002-18, Department of Information Technology, Uppsala University (2002)
Björklund, H., Sandberg, S., Vorobyov, S.: Complexity of Model Checking by Iterative Improvement: the Pseudo-Boolean Framework. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 381–394. Springer, Heidelberg (2004)
Borchers, B.: Csdp, a c library for semidefinite programming. In: Optimization Methods and Software, vol. 11, p. 613. Taylor and Francis, Abington (1999)
Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005)
Esparza, J., Gawlitza, T., Kiefer, S., Seidl, H.: Approximative methods for monotone systems of min-max-polynomial equations. In: Aceto et al. [1], pp. 698–710, ISBN 978-3-540-70574-1
Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 324–335. Springer, Heidelberg (2006) ISBN 3-540-35907-9
Etessami, K., Wojtczak, D., Yannakakis, M.: Recursive stochastic games with positive rewards. In: Aceto et al. [1], pp.711–723, ISBN 978-3-540-70574-1
Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: Nicola [16], pp. 237–252, ISBN 978-3-540-71314-2
Gawlitza, T., Seidl, H.: Precise relational invariants through strategy iteration. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 23–40. Springer, Heidelberg (2007) ISBN 978-3-540-74914-1
Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: Nicola [16], pp. 300–315 (2007) ISBN 978-3-540-71314-2
Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. Technical report, TUM (2009)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001) ISBN 3-540-42068-1
Miné, A.: The octagon abstract domain. In: WCRE, p. 310(2001)
De Nicola, R. (ed.): ESOP 2007. LNCS, vol. 4421. Springer, Heidelberg (2007) ISBN 978-3-540-71314-2
Ortega, J., Rheinboldt, W.: Iterative solution of nonlinear equations in several variables. Academic Press, London (1970)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005) ISBN 3-540-24297-X
Todd, M.J.: Semidefinite optimization. Acta Numerica 10, 515–560 (2001)
Wojtczak, D., Etessami, K.: Premo: An analyzer for probabilistic recursive models. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 66–71. Springer, Heidelberg (2007) ISBN 978-3-540-71208-4
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gawlitza, T.M., Seidl, H. (2010). Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely. In: Cousot, R., Martel, M. (eds) Static Analysis. SAS 2010. Lecture Notes in Computer Science, vol 6337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15769-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15769-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15768-4
Online ISBN: 978-3-642-15769-1
eBook Packages: Computer ScienceComputer Science (R0)