Abstract
We introduce a novel abstract domain for the safe approximation of continuous functions in the context of abstract interpretation-based static analysis. The key-idea is to represent \(\mathcal{C}_+^2\) functions by a finite sequence of trapezoids. In this way, we get a strictly more precise approximation of the actual values with respect to existing approaches in the literature. Experimental results underline the effectiveness of the approach in terms of both precision and efficiency.
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
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007)
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: Proceedings of PLDI 2003. ACM (2003)
Bouissou, O., Goubault, E., Putot, S., Tekkal, K., Vedrine, F.: HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 620–626. Springer, Heidelberg (2009)
Bouissou, O., Martel, M.: GRKLib: a guaranteed runge-kutta library. In: Proceedings of SCAN 2007. IEEE Press (2007)
Bouissou, O., Martel, M.: Abstract Interpretation of the Physical Inputs of Embedded Programs. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 37–51. Springer, Heidelberg (2008)
Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Proceedings of POPL 2010. ACM (2010)
Chaudhuri, S., Gulwani, S., Lublinerman, R., NavidPour, S.: Proving programs robust. In: Proceedings of FSE 2011. ACM (2011)
Chou, F., Wang, C.M., Cheng, G.D.: Optimal bounding of curves by continuous piecewise linear functions. Engineering Optimization 21(4), 307–317 (1993)
Chua, L., Kang, S.M.: Section-wise piecewise-linear functions: Canonical representation, properties, and applications. Proceedings of the IEEE 65(6), 915–929 (1977)
Cortesi, A.: Widening operators for abstract interpretation. In: Proceedings of SEFM 2008. IEEE Press (2008)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977. ACM (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL 1979. ACM (1979)
Edalat, A., Lieutier, A.: Domain theory and differential calculus (functions of one variable). Mathematical Structures in Comp. Sci. 14(6) (2004)
Feret, J.: Static Analysis of Digital Filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: Proceedings of ERTS 2006 (2006)
Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of Linear Hybrid Systems by Means of Convex Approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994)
Hamlet, D.: Continuity in software systems. In: Proceedings of ISSTA 2002. ACM (2002)
Henzinger, T.A., Ho, P.-H.: A Note on Abstract Interpretation Strategies for Hybrid Automata. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 252–264. Springer, Heidelberg (1995)
Imai, H., Iri, M.: An optimal algorithm for approximating a piecewise linear function. Journal of Information Processing 9(3), 159–162 (1987)
Kahlert, C., Chua, L.: A generalized canonical piecewise-linear representation. IEEE Transactions on Circuits and Systems 37(3), 373–383 (1990)
Tomek, I.: Two algorithms for piecewise-linear continuous approximation of functions of one variable. IEEE Trans. Comput. 23(4), 445–448 (1974)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Costantini, G., Ferrara, P., Cortesi, A. (2012). Linear Approximation of Continuous Systems with Trapezoid Step Functions. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)