Abstract
We give a formal model for a first order functional language to be executed on a stack machine and for a bytecode verifier that performs two kinds of static verifications : a type analysis and a shape analysis, that are part of a system used to ensure resource bounds. Both are instances of a general data flow analyzer due to Kildall. The generic algorithm and both of its instances are certified with the Coq proof assistant.
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
Preview
Unable to display preview. Download preview PDF.
References
Arkoudas, K., Salcianu, A.: Machine-checkable correctness proofs for intra-procedural dataflow analyses. In: Compiler Optimization meets Compiler Verification (COCV 2005), Edinburgh, Scotland (2005)
Amadio, R.M., Coupet-Grimal, S., Dal-Zilio, S., Jakubiec, L.: A functional scenario for bytecode verification of resource bounds. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 265–279. Springer, Heidelberg (2004)
Balaa, A., Bertot, Y.: Fonctions récursives générales par itération en théorie des types. Journées Francophones pour les Langages Applicatifs (January 2002)
Barthe, G., Dufay, G., Jakubiec, L., de Sousa, S.M.: A formal correspondence between offensive and defensive javacard virtual machines. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, p. 32. Springer, Heidelberg (2002)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B.P., de Sousa, S.M.: A formal executable semantics of the javacard platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 302–319. Springer, Heidelberg (2001)
Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 66–81. Springer, Heidelberg (2005)
Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a Data Flow Analyser in Constructive Logic. In: FP5 IST thematic network IST-2001-38957 APPSEM II, Tallinn, Estonia (2004)
Goldberg, A.: A specification of java loading and bytecode verification. In: ACM Conference on Computer and Communications Security, pp. 49–58 (1998)
Kildall, G.A.: A unified approach to global program optimization. In: ACM Symposium on Principles of Programming Languages, pp. 194–206 (1973)
Klein, G., Nipkow, T.: Verified bytecode verifiers. Theoretical Computer Science 298, 583–626 (2003)
Leroy, X.: Java Bytecode Verification: Algorithms and Formalizations. Journal of Automated Reasoning 30(3-4), 235–269 (2003)
Marion, J.-Y.: Complexité implicite des calculs de la théorie à la pratique. PhD thesis, Habilitation à diriger des recherches, Universitè Nancy 2 (December 2000)
Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 347–363. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coupet-Grimal, S., Delobel, W. (2006). A Uniform and Certified Approach for Two Static Analyses. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_8
Download citation
DOI: https://doi.org/10.1007/11617990_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)