zbMATH — the first resource for mathematics

The abstract domain of trapezoid step functions. (English) Zbl 1387.68069
Summary: The trapezoid step functions (TSF) domain is introduced in order to approximate continuous functions by a finite sequence of trapezoids, adopting linear functions to abstract the upper and the lower bounds of a continuous variable in each time slot. The lattice structure of TSF is studied, showing how to build and compute a sound abstraction of a given continuous function. Experimental results underline the effectiveness of the approach in terms of both precision and efficiency with respect to the domain of interval valued step functions (IVSF).
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI
[1] Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the fourth ACM symposium on principles of programming languages, Los Angeles, California, USA; January 1977. p. 238-52.
[2] Cousot P, Cousot R. Systematic design of program analysis frameworks. In: Conference record of the sixth annual ACM symposium on principles of programming languages, San Antonio, Texas, USA; January 1979. p. 269-82. · Zbl 1323.68356
[3] Bouissou O, Martel M. Abstract interpretation of the physical inputs of embedded programs. In: Verification, model checking, and abstract interpretation, in: Proceedings of the 9th international conference, VMCAI 2008, lecture notes in computer science, vol. 4905. San Francisco, USA: Springer; January 7-9, 2008. p. 37-51. · Zbl 1138.68358
[4] Costantini G, Ferrara P, Cortesi A. Linear approximation of continuous systems with trapezoid step functions. In: Proceedings of the 10th asian symposium on programming languages and systems, APLAS 2012, lecture notes in computer science, vol. 7705. Kyoto, Japan: Springer; December 11-13, 2012. p. 98-114.
[5] Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Conference record of the fifth annual ACM symposium on principles of programming languages. Tucson, Arizona, USA: ACM Press; January 1978. p. 84-96.
[6] Miné, A., The octagon abstract domain, Higher-order symb comput, 19, 31-100, (2006) · Zbl 1105.68069
[7] Aubin, J.P.; Cellina, A., Differential inclusions: set-valued maps and viability theory, (1984), Springer-Verlag New York · Zbl 0538.34007
[8] Bressan, A.; Cortesi, A., Directionally continuous selections in Banach spaces, Nonlinear anal, theory, methods appl, 13, 987-992, (1989) · Zbl 0687.34013
[9] Goubault E, Martel M, Putot S. Some future challenges in the validation of control systems. In: Proceedings of the European congress on embedded real time software, ERTS ׳06; 2006. p. 1-11.
[10] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, et al. Combination of abstractions in the astrée static analyzer. In: 11th Asian computing science conference on advances in computer science, ASIAN 2006, December 6-8, 2006, lecture notes in computer science, vol. 4435. Tokyo, Japan: Springer; 2008. p. 272-300.
[11] Bagnara, R.; Hill, P.M.; Zaffanella, E., Weakly-relational shapes for numeric abstractionsimproved algorithms and proofs of correctness, Form methods syst des, 35, 279-323, (2009) · Zbl 1185.68405
[12] Cortesi A. Widening operators for abstract interpretation. In: Sixth IEEE international conference on software engineering and formal methods, SEFM 2008. Cape Town, South Africa: IEEE Computer Society; 10-14 November 2008. p. 31-40.
[13] Cortesi, A.; Zanioli, M., Widening and narrowing operators for abstract interpretation, Comput lang, syst struct, 37, 24-42, (2011) · Zbl 1218.68100
[14] Urban C. The abstract domain of segmented ranking functions. In: Proceedings of the 20th international static analysis symposium SAS, lecture notes in computer science, vol. 7935. Seattle, WA, USA: Springer; 2013. p. 43-62.
[15] Costantini, G.; Ferrara, P.; Cortesi, A., A suite of abstract domains for static analysis of string values, Softw, pract exp, 45, 245-287, (2015)
[16] Bouissou O, Martel M. GRKLib: a guaranteed runge-kutta library. In: Follow-up of international symposium on scientific computing, computer arithmetic and validated numerics. Duisburg:IEEE Press; 2007.
[17] Bouissou O, Goubault E, Putot S, Tekkal K, Védrine F. Hybridfluctuat: a static analyzer of numerical programs within a continuous environment. In: Proceedings of the CAV ׳09, lecture notes in computer science. Grenoble, France:Springer; 2009.
[18] Edalat, A.; Lieutier, A., Domain theory and differential calculus (functions of one variable), Math struct comput sci, 14, (2004) · Zbl 1062.03037
[19] Feret J. Static analysis of digital filters. In: Proceedings of the 13th European symposium on programming, ESOP 2004, lecture notes in computer science, vol. 2986. p. 33-48. · Zbl 1126.68347
[20] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, et al. A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation. San Diego, California, USA: ACM Press; June 9-11, 2003. p. 196-207. · Zbl 1026.68514
[21] Halbwachs N, Proy Y-E, Raymond P. Verification of linear hybrid systems by means of convex approximations. In: Proceedings of the static analysis symposium, SAS ׳94, lecture notes in computer science, vol. 818. Namur, Belgium:Springer; 1994. p. 223-37.
[22] Henzinger TA, Ho P-H. A note on abstract interpretation strategies for hybrid automata. In: Hybrid systems II. Springer-Verlag; 1995. p. 252-64.
[23] Hamlet D. Continuity in software systems. In: Proceedings of the international symposium on software testing and analysis. Roma, Italy: ACM; July 22-24, 2002; ISSTA. p. 196-200.
[24] Reed J, Pierce BC. Distance makes the types grow stronger: a calculus for differential privacy. In: Proceedings of the 15th ACM SIGPLAN international conference on functional programming, ICFP ׳10. New York, NY, USA: ACM; 2010. p. 157-68. · Zbl 1323.68254
[25] Chaudhuri S, Gulwani S, Lublinerman R. Continuity analysis of programs. In: Proceedings of the 37th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2010. Madrid, Spain; January 17-23; 2010. p. 57-70. · Zbl 1312.68056
[26] Chaudhuri S, Gulwani S, Lublinerman R, NavidPour S. Proving programs robust. In: SIGSOFT/FSE׳11 - 19th ACM SIGSOFT symposium on the foundations of software engineering (FSE-19) and ESEC׳11 - 13th European software engineering conference (ESEC-13). Szeged, Hungary; September 5-9, 2011. p. 102-12.
[27] Chua, L.; Kang, S.M., Section-wise piecewise-linear functionscanonical representation, properties, and applications, Proc IEEE, 65, 915-929, (1977)
[28] Kahlert, C.; Chua, L., A generalized canonical piecewise-linear representation, IEEE trans circuits syst, 37, 373-383, (1990) · Zbl 0704.94026
[29] Chou, F.; Wang, C.M.; Cheng, G.D., Optimal bounding of curves by continuous piecewise linear functions, Eng optim, 21, 307-317, (1993)
[30] Imai, H.; Iri, M., An optimal algorithm for approximating a piecewise linear function, J inf process, 9, 159-162, (1987) · Zbl 0631.65010
[31] Tomek, I., Two algorithms for piecewise-linear continuous approximation of functions of one variable, IEEE trans comput, 23, 445-448, (1974) · Zbl 0284.68078
[32] Albert E, Arenas P, Genaim S, Puebla G, Zanardini D. Cost analysis of java bytecode. In: Proceedings of the 16th European symposium on Programming languages and systems, ESOP 2007, held as part of the joint European conferences on theory and practics of software, ETAPS 2007, lecture notes in computer science, vol. 4421. Braga, Portugal: Springer; March 24-April 1, 2007. p. 157-72. · Zbl 1236.68042
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.