Advertisement

Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT

  • Eric Goubault
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

This invited lecture is a survey of our work over the last 12 years or so, dealing with the precise analysis of numerical programs, essentially control programs such as the ones found in the aerospace, nuclear and automotive industry.

Our approach is now based on a rather generic abstract domain, based on “zonotopes” or “affine forms” [7], but with some specificities. For instance, our zonotopic domain provides a functional abstraction [16,13], i.e. an abstraction of the input-output relationships between values of variables, allowing for test generation and modular verification [21]. Also, our domain deals with the real number and the finite precision (for instance, floating-point or fixed-point) semantics [14,17]. It is used in practice in FLUCTUAT [20,9,4] to prove some functional properties of programs, generate (counter-) examples, identify the discrepancy between the real number and the finite precision semantics and its origin etc.

Keywords

Abstract Interpretation Concurrent Program Policy Iteration Abstract Domain Numerical Program 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Adjé, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., Putot, S.: Analyzing probabilistic programs with partially known distributions. In: VSTTE (2013)Google Scholar
  2. 2.
    Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Logical Methods in Computer Science 8(1) (2012)Google Scholar
  3. 3.
    Boldo, S., Filliâtre, J.C.: Formal Verification of Floating-Point Programs. In: 18th IEEE International Symposium on Computer Arithmetic (June 2007)Google Scholar
  4. 4.
    Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Ghorbal, K., Lesens, D., Putot, S., Turin, M.: Space software validation using abstract interpretation. In: DASIA (2009)Google Scholar
  5. 5.
    Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2-4), 189–201 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: Proceedings of SIBGRAPI (1993)Google Scholar
  8. 8.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)Google Scholar
  9. 9.
    Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Fajstrup, L., Goubault, É., Haucourt, E., Mimram, S., Raussen, M.: Trace spaces: An efficient new technique for state-space reduction. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 274–294. Springer, Heidelberg (2012)Google Scholar
  11. 11.
    Gawlitza, T.M., Seidl, H., Adjé, A., Gaubert, S., Goubault, E.: Abstract interpretation meets convex optimization. J. Symb. Comput. 47(12), 1416–1446 (2012)zbMATHCrossRefGoogle Scholar
  12. 12.
    Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212–226. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Goubault, E., Gall, T.L., Putot, S.: An accurate join for zonotopes, preserving affine input/output relations. In: Proceedings of NSAD 2012, 4th Workshop on Numerical and Symbolic Abstract Domains. ENTCS, vol. 287, pp. 65–76 (2012)Google Scholar
  14. 14.
    Goubault, É., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Goubault, E., Putot, S.: Under-approximations of computations in real numbers based on generalized affine arithmetic. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 137–152. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. CoRR abs/0910.1763 (2009), http://arxiv.org/abs/0910.1763
  17. 17.
    Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  18. 18.
    Goubault, É.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 234–259. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Goubault, E., Haucourt, E.: A practical application of geometric semantics to static analysis of concurrent programs. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 503–517. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 3–20. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Goubault, E., Putot, S., Védrine, F.: Modular static analysis with zonotopes. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 24–40. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  22. 22.
    Menard, D., Rocher, R., Sentieys, O., Simon, N., Didier, L.S., Hilaire, T., Lopez, B., Goubault, E., Putot, S., Védrine, F., Najahi, A., Revy, G., Fangain, L., Samoyeau, C., Lemonnier, F., Clienti, C.: Design of fixed-point embedded systems (defis) french anr project. In: DASIP, pp. 1–2 (2012)Google Scholar
  23. 23.
    Meurant, G.: The Lanczos and Conjugate Gradient Algorithms: From Theory to Finite Precision Computations (Software, Environments, and Tools). SIAM (2006)Google Scholar
  24. 24.
    Paige, C.C.: The computation of eigenvalues and eigenvectors of very large sparse matrices. Ph.D. thesis (1971)Google Scholar
  25. 25.
    Wilkinson, J.H.: The algebraic eigenvalue problem. Oxford University Press (1965)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Eric Goubault
    • 1
  1. 1.CEA Saclay, NanoinnovCEA LISTGif-sur-Yvette CEDEXFrance

Personalised recommendations