Abstract
The precision of an analysis based on abstract interpretation does not only depend on the abstract domain, but also on the solving method. The traditional solution is to solve iteratively abstract fixpoint equations, using extrapolation with a widening operator to make the iterations converge. Unfortunately, this extrapolation often loses crucial information for the analysis goal. A classical technique for improving the precision is “widening with thresholds”, which bounds the extrapolation. Its benefit strongly depends on the choice of relevant thresholds. In this paper we propose a semantic-based technique for automatically inferring such thresholds, which applies to any control graph, be it intraprocedural, interprocedural or concurrent, without specific assumptions on the abstract domain. Despite its technical simplicity, our technique is able to infer the relevant thresholds in many practical cases.
This work was supported by the OpenTLM project (pôle de compétitivité Minalogic).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Su, Z., Wagner, D.: A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 280–295. Springer, Heidelberg (2004)
Gawlitza, T., Leroux, J., Reineke, J., Seidl, H., Sutre, G., Wilhelm, R.: Polynomial precise interval analysis revisited. In: Albers, S., Alt, H., Näher, S. (eds.) EA 2009. LNCS, vol. 5760, pp. 422–437. Springer, Heidelberg (2009)
Costan, A., Gaubert, S., Goubault, É., 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)
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)
Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11 (1997)
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Miné, A.: The octagon abstract domain. In: Higher-Order and Symbolic Computation, vol. 19 (2006)
Bagnara, R., Hill, P.M., Ricci, E., Zafanella, E.: Precise widening operators for convex polyhedra. In: Science of Computer Programming (SCP), vol. 58 (2005)
Simon, A., Chen, L.: Simple and precise widenings for polyhedra. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 139–155. Springer, Heidelberg (2010)
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.W.: Guided static analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349–365. Springer, Heidelberg (2007)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does astrée scale up? Formal Methods in System Design 35 (2009)
Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. Rapport de recherche RR-7673, INRIA (2011)
Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)
Halbwachs, N.: A heuristics for inferring thresholds (personal communication)
Jeannet, B.: The bddapron logico-numerical abstract domains library, http://www.inrialpes.fr/pop-art/people/bjeannet/bjeannet-forge/bddapron/
Jeannet, B.: The ConcurInterproc interprocedural analyzer for concurrent programs, http://pop-art.inrialpes.fr/interproc/concurinterprocweb.cgi
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the astrée static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lakhdar-Chaouch, L., Jeannet, B., Girault, A. (2011). Widening with Thresholds for Programs with Complex Control Graphs. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)