Abstract
Static analysers are becoming so complex that it is crucial to ascertain the soundness of their results in a provable way. In this paper we develop a certified checker in Coq that is able to certify the results of a polyhedral array-bound analysis for an imperative, stack-oriented bytecode language with procedures, arrays and global variables. The checker uses, in addition to the analysis result, certificates which at the same time improve efficiency and make correctness proofs much easier. In particular, our result certifier avoids complex polyhedral computations such as convex hulls and is using easily checkable inclusion certificates based on Farkas lemma. Benchmarks demonstrate that our approach is effective and produces certificates that can be efficiently checked not only by an extracted Caml checker but also directly in Coq.
This work was partially funded by the FET Global Computing project Mobius, by the Brittany region project CertLogS and the FRAE project Ascert.
Chapter PDF
References
Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 95–105. IEEE Computer Society, Los Alamitos (1990)
Barthe, G., Dufay, G.: A tool-assisted framework for certified bytecode verification. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 99–113. Springer, Heidelberg (2004)
Besson, F.: Fast reflexive arithmetic tactics: the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2006)
Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Research Report 6333, Inria (2007), http://hal.inria.fr/inria-00166930/
Besson, F., Jensen, T., Turpin, T.: Small witnesses for abstract interpretation based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 268–283. Springer, Heidelberg (2007)
Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science 342(1), 56–78 (2005)
Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. U.S.S.R Comp. Mathematics and Mathematical Physics 5(2), 228–233 (1965)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints. In: Proc. of 4th ACM Symp. on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
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: Proc. of 5th ACM Symp. on Principles of Programming Languages (POPL 1978), pp. 84–97. ACM Press, New York (1978)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM international conference on Functional programming (ICFP 2002), pp. 235–246. ACM Press, New York (2002)
Jeannet, B., the Apron team: The Apron library (2007)
Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science 298(3), 583–626 (2002)
Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: Proc. of 34th ACM Symp. on Principles of Programming Languages (POPL 2007), pp. 173–184. ACM Press, New York (2007)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proc. of the 33rd ACM Symp. on Principles of Programming Languages, pp. 42–54. ACM Press, New York (2006)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19, 31–100 (2006)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. of 31st ACM Symp. on Principles of Programming Languages (POPL 2004), pp. 330–341. ACM Press, New York (2004)
Pichardie, D.: Interprétation abstraite en logique intuitioniste: extraction d’analyseurs Java certifiés. PhD thesis, Université de Rennes 1 (2005)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)
Wasserman, H., Blum, M.: Software reliability via run-time result-checking. Journal of the ACM 44(6), 826–849 (1997)
Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Proc. of 1st Workshop on Bytecode Semantics, Verification and Transformation, ENTCS (2005)
Wildmoser, M., Nipkow, T.: Asserting bytecode safety. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 326–341. Springer, Heidelberg (2005)
The Coq development of the work, http://www.irisa.fr/celtique/ext/polycert/
Xi, H.: Imperative Programming with Dependent Types. In: Proc. of 15th IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 375–387. IEEE, Los Alamitos (2000)
Xi, H., Xia, S.: Towards Array Bound Check Elimination in Java Virtual Machine Language. In: Proc. of CASCOON 1999, pp. 110–125 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Besson, F., Jensen, T., Pichardie, D., Turpin, T. (2010). Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds) Trustworthly Global Computing. TGC 2010. Lecture Notes in Computer Science, vol 6084. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15640-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15640-3_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15639-7
Online ISBN: 978-3-642-15640-3
eBook Packages: Computer ScienceComputer Science (R0)