Abstract
While the definition of the revised widening for polyhedra is defined in terms of inequalities, most implementations use the double description method as a means to an efficient implementation. We show how standard widening can be implemented in a simple and efficient way using a normalized H-representation (constraint-only) which has become popular in recent approximations to polyhedral analysis. We then detail a novel heuristic for this representation that is tuned to capture linear transformations of the state space while ensuring quick convergence for non-linear transformations for which no precise linear invariants exist.
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
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise Widening Operators for Convex Polyhedra. Science of Computer Programming 58(1-2), 28–56 (2005)
Benoy, F.: Polyhedral Domains for Abstract Interpretation in Logic Programming. PhD thesis, Computing Lab., University of Kent, Canterbury, UK (January 2002)
Besson, F., Jensen, T.P., Talpin, J.-P.: Polyhedral Analysis for Synchronous Languages. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51–68. Springer, Heidelberg (1999)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Programming Language Design and Implementation, San Diego, Calif., USA. ACM, New York (June 2003)
Chen, L., Miné, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3–18. Springer, Heidelberg (2008)
Chen, L., Miné, A., Wang, J., Cousot, P.: An abstract domain to discover interval linear equalities. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 112–128. Springer, Heidelberg (2010)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Constraints among Variables of a Program. In: Principles of Programming Languages, Tucson, Arizona, USA, pp. 84–97. ACM, New York (January 1978)
Gonnord, L., Halbwachs, N.: Combining Widening and Acceleration in Linear Relation Analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006)
Gopan, D., Reps, T.: Lookahead Widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)
Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3eme cicle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (March 1979)
Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993)
Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of Linear Hybrid Systems by Means of Convex Approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864. Springer, Heidelberg (September 1994)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Howe, J.M., King, A.: Logahedra: a New Weakly Relational Domain. In: Lu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306–320. Springer, Heidelberg (2009)
Imbert, J.L., Van Hentenryck, P.: Redundancy Elimination with a Lexicographic Solved Form. Technical Report CS-95-02, Brown University, Providence, Rhode Island, USA (1995)
Mesnard, F., Bagnara, R.: cTI: a Constraint-Based Termination Inference Tool for ISO-Prolog. Theory and Practice of Logic Programming 5(1-2), 243–257 (2005)
Miné, A.: The Octagon Abstract Domain. In: Conference on Reverse Engineering, Stuttgart, Germany, pp. 310–319. IEEE Computer Society, Los Alamitos (October 2001)
Sankaranarayanan, S., Colón, M., Sipma, H.B., Manna, Z.: Efficient Strongly Relational Polyhedral Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111–125. Springer, Heidelberg (2005)
Simon, A., King, A.: Exploiting Sparsity in Polyhedral Analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005)
Simon, A., King, A.: Widening Polyhedra with Landmarks. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 166–182. Springer, Heidelberg (2006)
Simon, A., King, A., Howe, J.M.: Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664. Springer, Heidelberg (2003)
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
Simon, A., Chen, L. (2010). Simple and Precise Widenings for H-Polyhedra. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)