Abstract
Verifying properties of large real-world programs requires vast quantities of information on aspects such as procedural contexts, loop invariants or pointer aliasing. It is unimaginable to have all these properties provided to a verification tool by annotations from the user. Static analysis will clearly play a key role in the design of future verification engines by automatically discovering the bulk of this information. The body of research in static program analysis can be split up in two major areas: one-probably the larger in terms of publications-is concerned with discovering properties of data structures (shape analysis, pointer analysis); the other addresses the inference of numerical invariants for integer or floating-point algorithms (range analysis, propagation of round-off errors in numerical algorithms).We will call the former ”symbolic static analysis” and the latter ”numerical static analysis”. Both areas were successful in effectively analyzing large applications [16,6,11,2,4]. However, symbolic and numerical static analysis are commonly regarded as entirely orthogonal problems. For example, a pointer analysis usually abstracts away all numerical values that appear in the program, whereas the floating-point analysis tool ASTREE [2,4] does not abstract memory at all.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, L.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)
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 the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), June 7–14, 2003, pp. 196–207. ACM Press, New York (2003)
Brat, G., Venet, A.: Precise and scalable static program analysis of NASA flight software. In: Proceedings of the 2005 IEEE Aerospace Conference (2005)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE Analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the Fifth Conference on Principles of Programming Languages, ACM Press, New York (1978)
Das, M.: Unification-based pointer analysis with directional assignments. ACM SIGPLAN Notices 35(5), 35–46 (2000)
de Moura, L., Owre, S., Ruess, H., Rushby, J., Shankar, N.: Integrating verification components. In: Verified Software: Theories, Tools, Experiments, Zürich, Switzerland (October, 2005)
Deutsch, A.: A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations. In: Proceedings of the 1992 International Conference on Computer Languages, pp. 2–13. IEEE Computer Society Press, Los Alamitos (1992)
Deutsch, A.: Interprocedural alias analysis for pointers: beyond k-limiting. In: ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, ACM Press, New York (1994)
Eilenberg, S.: Automata, Languages and Machines, vol. A. Academic Press, London (1974)
Heintze, N., Tardieu, O.: Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 254–263 (2001)
Karr, M.: Affine relationships among variables of a program. Acta Informatica, 133–151 (1976)
Kestrel,: Specware System and documentation (2003), http://www.specware.org/
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, Heidelberg (1992)
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)
Steensgaard, B.: Points-to analysis by type inference of programs with structures and unions. In: Computational Complexity, pp. 136–150 (1996)
Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 266–382. Springer, Heidelberg (1996)
Venet, A.: Abstract interpretation of the π-calculus. In: Dam, M. (ed.) LOMAPS-WS 1996. LNCS, vol. 1192, pp. 51–75. Springer, Heidelberg (1997)
Venet, A.: Automatic determination of communication topologies in mobile systems. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 152–167. Springer, Heidelberg (1998)
Venet, A.: Automatic analysis of pointer aliasing for untyped programs. Science of Computer Programming 35(2), 223–248 (1999)
Venet, A.: Nonuniform alias analysis of recursive data structures and arrays. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 36–51. Springer, Heidelberg (2002)
Venet, A.: A scalable nonuniform pointer analysis for embedded programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 149–164. Springer, Heidelberg (2004)
Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the International Conference on Programming Language Design and Implementation, pp. 231–242 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Venet, A. (2008). Towards the Integration of Symbolic and Numerical Static Analysis. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)