×

A zonotopic framework for functional abstractions. (English) Zbl 1331.68050

Summary: This article fully describes an abstract domain, dedicated to the generation of accurate numerical invariants and based on zonotopes parameterized by vectors of affine forms. We introduce the abstract transfer functions, prove their correctness and demonstrate their efficiency. One strength of the domain is its simple abstraction of non-linear operations. These affine vectors also abstract input/output relations, which allows in particular modular analysis, proofs of user-defined complex invariants and test case generation. Finally, the affine vectors like parametrization is flexible enough to allow variations that yield different interesting abstractions, such as inner-approximations or abstraction of probabilistic information.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Apron; PPL; NewPolka
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Adjé A, Bouissou O, Goubault-Larrecq J, Goubault E, Putot S (2014) Static analysis of programs with imprecise probabilistic inputs. In: Verified software: theories, tools, experiments—5th international conference, VSTTE 2013, Lecture notes in computer science, vol 8164. Springer, pp 22-47
[2] Adje A, Gaubert S, Goubault E (2010) Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Proceedings of the European symposium on programming. Springer · Zbl 1260.68082
[3] Alamo T, Bravo J, Camacho E (2005) Guaranteed state estimation by zonotopes. Automatica 41(6):1035-1043. doi:10.1016/j.automatica.2004.12.008 · Zbl 1091.93038 · doi:10.1016/j.automatica.2004.12.008
[4] Althoff M, Krogh BH (2011) Zonotope bundles for the efficient computation of reachable sets. Proc CDC 2011:6814-6821
[5] Althoff M, Krogh BH (2014) Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans Autom Control 59(2):371-383 · Zbl 1360.93082 · doi:10.1109/TAC.2013.2285751
[6] Bagnara R, Ricci E, Zaffanella E, Hill PM (2002) Possibly not closed convex polyhedra and the parma polyhedra library. In: SAS ’02: proceedings of the 9th international symposium on static analysis, Springer, London, pp 213-229. http://www.cs.unipr.it/ppl/ · Zbl 1015.68215
[7] Bertsekas DP, Nedic A, Ozdaglar AE (2003) Convex analysis and optimization. Athena Scientific, Belmont · Zbl 1140.90001
[8] Bouissou O, Goubault E, Goubault-Larrecq J, Putot S (2012) A generalization of p-boxes to affine arithmetic. Computing 94:1-13 · Zbl 1247.60006 · doi:10.1007/s00607-011-0182-8
[9] Chatterjee R, Ryder BG, Landi WA (1999) Relevant context inference. In: POPL ’99: proceedings of the 26th ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, pp 133-146. http://doi.acm.org/10.1145/292540.292554
[10] Comba JLD, Stolfi J (1993) Affine arithmetic and its applications to computer graphics. In: VI Simpósio Brasileiro de Computação Gráfica e Processamento de Imagens (SIBGRAPI’93), pp 9-18
[11] Combastel C (2003) A state bounding observer based on zonotopes. In: Proceedings of european control conference. Cambridge
[12] Combastel C (2005) A state bounding observer for uncertain non-linear continuous-time systems based on zonotopes. In: Proceedings of 44th IEEE conference on decision and control
[13] Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: CAV, pp 462-475 · Zbl 1081.68616
[14] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximations of fixed points. Princ Prog Lang 4:238-252
[15] Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Logic Comput 2(4):511-547 · Zbl 0783.68073 · doi:10.1093/logcom/2.4.511
[16] Cousot P, Cousot R (1993) Galois connection based abstract interpretations for strictness analysis, invited paper. In: Bjørner D, Broy M, Pottosin I (eds) Proceedings of the international conference on formal methods in programming and their applications, Academgorodok. Lecture notes in computer science vol 735. Springer, Berlin, pp 98-127. doi:10.1007/BFb0039703 · Zbl 0788.68094
[17] Cousot P, Cousot R (2001) Compositional separate modular static analysis of programs by abstract interpretation. In: Proceedings of the Second international conference on advances in infrastructure for e-business, e-science and e-education on the internet, SSGRR 2001. Scuola Superiore G. Reiss Romoli, Compact disk, L’Aquila · Zbl 1260.68089
[18] Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL, pp 84-96 · Zbl 1360.93082
[19] Delmas D, Goubault E, Putot S, Souyris J, Tekkal K, Védrine F (2009) Towards an industrial use of fluctuat on safety-critical avionics software. In: Proceedings of FMICS, LNCS, vol. 5825
[20] Feret J (2004) Static analysis of digital filters. In: Proceedings of ESOP, LNCS, vol. 2986. Springer · Zbl 1126.68347
[21] de Figueiredo LH, Stolfi J (2004) Affine arithmetic: concepts and applications. Numer Algorithms 37(1-4):147-158 · Zbl 1074.65050 · doi:10.1023/B:NUMA.0000049462.70970.b6
[22] Gaubert S, Goubault E, Taly A, Zennou S (2007) Static analysis by policy iteration on relational domains. In: Proceedings of the Sixteenth european symposium of programming (ESOP’07), LNCS, vol. 4421, Springer, pp 237-252 · Zbl 1187.68151
[23] Ghorbal K, Goubault E, Putot S (2009) The zonotope abstract domain taylor1+. In: CAV ’09: proceedings of the 21st international conference on computer aided verification, Springer, Berlin/Heidelberg, pp 627-633. doi:10.1007/978-3-642-02658-4_47 · Zbl 0783.68073
[24] Ghorbal K, Goubault E, Putot S (2010) A logical product approach to zonotope intersection. In: CAV’10: Proceedings of the 22nd international conference on computer aided verification, LNCS, vol. 6174. Springer, Berlin/Heidelberg
[25] Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Proceeedings of HSCC 2005, LNCS, vol 3414, pp 291-305 · Zbl 1078.93005
[26] Girard A, Le Guernic C (2008) Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: HSCC ’08: proceedings of the 11th international workshop on hybrid systems, Springer, Berlin, Heidelberg, pp 215-228. doi:10.1007/978-3-540-78929-1_16 · Zbl 1144.93324
[27] Goubault E, Gall TL, Putot S (2012) An accurate join for zonotopes, preserving affine input/output relations. In: Proceedings of NSAD’12, ENTCS, vol 287, pp 65-76 · Zbl 1294.68055
[28] Goubault E, Mullier O, Putot S, Kieffer M (2014) Inner approximated reachability analysis. In: HSCC’14, ACM, pp 163-172 · Zbl 1362.93016
[29] Goubault E, Putot S (2006) Static analysis of numerical algorithms. In: Yi K (ed) SAS, Lecture notes in computer science, vol 4134, Springer, pp 18-34 · Zbl 1225.68073
[30] Goubault E, Putot S (2007) Under-approximations of computations in real numbers based on generalized affine arithmetic. In: Nielson HR, Filé G (eds) SAS, Lecture notes in computer science, vol 4634, Springer, pp 137-152 · Zbl 1211.68088
[31] Goubault E, Putot S (2008) Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR abs/0807.2961
[32] Goubault E, Putot S (2009) A zonotopic framework for functional abstractions. CoRR abs/0910.1763 · Zbl 1331.68050
[33] Goubault E, Putot S (2011) Static analysis of finite precision computations. In: Proceedings of verification, model checking, and abstract interpretation—12th international conference, VMCAI 2011, LNCS, vol 6538, Austin, pp 232-247 · Zbl 1317.68116
[34] Goubault E, Putot S (2013) Robustness analysis of finite precision implementations. In: Proceedings of APLAS, Lecture notes in computer science, vol 8301, Springer, pp 50-57 · Zbl 06385641
[35] Goubault E, Putot S, Baufreton P, Gassino J (2007) Static analysis of the accuracy in control systems: principles and experiments. In: Leue S, Merino P (eds) FMICS, Lecture notes in computer science, vol 4916, Springer, pp 3-20
[36] Goubault E, Putot S, Védrine F (2012) Modular static analysis with zonotopes. In: Proceedings on static analysis—19th international symposium, SAS 2012, Deauville, 11-13 September 2012. pp 24-40
[37] Guernic CL, Girard A (2009) Reachability analysis of hybrid systems using support functions. In: CAV, pp 540-554 · Zbl 1242.93059
[38] Guibas LJ, Nguyen A, Zhang L (2003) Zonotopes as bounding volumes. In: SODA, pp 803-812 · Zbl 1092.68697
[39] Jeannet B, al. Newpolka library. http://www.inrialpes.fr/pop-art/people/bjeannet/newpolka
[40] Jeannet B, Gopan D, Reps T (2005) A relational abstraction for functions. In: International workshop on numerical and symbolic abstract domains · Zbl 1141.68371
[41] Jeannet B, Miné A (2009) Apron: A library of numerical abstract domains for static analysis. In: CAV, pp 661-667
[42] Kühn, W.; Hege, HC (ed.); Polthier, K. (ed.), Zonotope dynamics in numerical quality control, 125-134 (1998), Heidelberg · Zbl 0940.68152 · doi:10.1007/978-3-662-03567-2_10
[43] Kurzhanski AB, Varaiya P (2000) Ellipsoidal techniques for reachability analysis. In: HSCC ’00: proceedings of the third international workshop on hybrid systems: Computation and Control, Springer, pp 202-214 · Zbl 0962.93009
[44] Kurzhanskii AB, Vlyi I (1997) Ellipsoidal calculus for estimation and control. Laxenburg, Austria : IIASA; Boston : Birkhuser Boston
[45] Le VTH, Stoica C, Alamo T, Camacho E, Dumur D (2013) Zonotopes: from guaranteed state estimation to control. Wiley-ISTE, Hoboken · doi:10.1002/9781118761588
[46] Miné A (2001) A new numerical abstract domain based on difference-bound matrices. In: PADO ’01: proceedings of the second symposium on programs as data objects, Springer, London, pp 155-172 · Zbl 0984.68034
[47] Miné A (2006) Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI’06, pp 348-363 · Zbl 1176.68050
[48] Monniaux D (2005) Compositional analysis of floating-point linear numerical filters. In: CAV, pp 199-212 · Zbl 1081.93028
[49] Rump S, Kashiwagi M (2014) Implementation and improvements of affine arithmetic. Nonlinear Theory Appl 2:1101-1119 · Zbl 1331.92134
[50] Ziegler GM (2007) Lectures on polytopes (updated seventh printing). No. 152 in graduate texts in mathematics. Springer, New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.