Apron: A Library of Numerical Abstract Domains for Static Analysis

1. The APRON abstract domain library, http://apron.cri.ensmp.fr/library/

2. GMP: The GNU multiple precision arithmetic library, http://gmplib.org/

3. The MPFR library, http://www.mpfr.org/

4. Amjad, H., Bornat, R.: Towards automatic stability analysis for rely-guarantee proofs. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 14–28. Springer, Heidelberg (2009)

   Google Scholar 

5. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. SCP 72(1-2), 3–21 (2008)

   MathSciNet  Google Scholar 

6. Chen, L., Miné, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3–18. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

7. Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312–327. Springer, Heidelberg (2004)

   Chapter  Google Scholar 

8. IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Technical report, ANSI/IEEE Std. 745-1985 (1985)

   Google Scholar 

9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252. ACM Press, New York (1977)

   Google Scholar 

10. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84–97. ACM Press, New York (1978)

    Google Scholar 

11. Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, S.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 512–529. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

12. Granger, P.: Static analysis of arithmetical congruences. Int. Journal of Computer Mathematics 30, 165–190 (1989)

    Article  MATH  Google Scholar 

13. Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991)

    Google Scholar 

14. Jeannet, B.: The Fixpoint solver, http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint/

15. Jeannet, B., et al.: The Interproc analyzer, http://pop-art.inrialpes.fr/interproc/interprocweb.cgi

16. Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 258–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

17. Karr, M.: Affine relationships among variables of a program. Acta Informatica, 133–151 (1976)

    Google Scholar 

18. Majumdar, R., Gupta, A., Rybalchenko, A.: An efficient invariant generator. In: Federrath, H. (ed.) Designing Privacy Enhancing Technologies. LNCS, vol. 2009. Springer, Heidelberg (2001)

    Google Scholar 

19. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

20. Miné, A.: The octagon abstract domain. HOSC 19(1), 31–100 (2006)

    MATH  Google Scholar 

21. Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In: Leuschel, M.A. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references