Abstract
In static analysis, the choice of an adequate abstract domain is an interesting issue. In this paper, we provide a new numerical abstract domain: 4-Octahedron. It is an Octahedra subclass that infers relations of the form: { \( x \sim \alpha , x-y \sim \beta , (x-y) - (z-t) \sim \lambda \)}, such that: x, y, z and t are real variables, \(\alpha , \beta \) and \( \lambda \) are real constants and \({\sim }\in \{\le ,\ge \}\). Its precision lies between the octagons and octahedra. We construct a suitable structure for its representation, we provide normalization algorithms for computing its canonical form and we give methods to compute its transfer functions (Union, Intersection, Assignment, Projection, ...). Complexity of the implementation algorithms is proved to be polynomial.
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
Similar content being viewed by others
References
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: SPPL, pp. 238–252. ACM Press (1977)
Goubault, É., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Timed Specifications: Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1989)
Miné, A.: The octagon abstract domain. In: Proceedings of Analysis, Slicing and Tranformation, pp. 310–319. IEEE CS Press (2001)
Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87–90 (1958)
Clarisò, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64, 115–139 (2007)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Methods Syst. Des. 11, 157–185 (1997)
Benes, N., Bezdek, P., Larsen, K.G., Srba, J. Language Emptiness of Continuous-Time Parametric Timed Automata (2015). arXiv preprint arXiv:1504.07838
André, É., Markey, N.: Language preservation problems in parametric timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 27–43. Springer, Heidelberg (2015)
Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 141–159. Springer, Heidelberg (2012)
Blunno, I., Cortadella, J., Kondratyev, A., Lavagno, L., Lwin, K., Sotiriou, C.: Handshake protocols for de-synchronization. In: The 10th International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 149–158 (2004)
The detailed proofs and explanations website: http://www.fsdmfes.ac.ma/Octahedron
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Oucheikh, R., Berrada, I., El Hichami, O. (2016). The 4-Octahedron Abstract Domain . In: Abdulla, P., Delporte-Gallet, C. (eds) Networked Systems. NETYS 2016. Lecture Notes in Computer Science(), vol 9944. Springer, Cham. https://doi.org/10.1007/978-3-319-46140-3_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-46140-3_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46139-7
Online ISBN: 978-3-319-46140-3
eBook Packages: Computer ScienceComputer Science (R0)