Abstract
We instantiate an Isabelle/HOL framework for proof carrying code to Jinja bytecode, a downsized variant of Java bytecode featuring objects, inheritance, method calls and exceptions. Bytecode annotated in a first order expression language can be certified not to produce arithmetic overflows. For this purpose we use a generic verification condition generator, which we have proven correct and relatively complete.
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
VeryPCC project website in Munich (2003), http://isabelle.in.tum.de/verypcc/
Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 11–41. Springer, Heidelberg (2004)
Appel, A.W.: Foundational proof-carrying code. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), June 2001, pp. 247–258 (2001)
Aspinall, D., Beringer, L., Hoffman, M., Loidl, H.-W.: A resource-aware program logic for a jvm-like language. In: Gilmore, S. (ed.) Trends in Functional Programming, Edinburgh (2003)
Boer, F.D., Pierik, C.: A syntax-directed hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 64–78. Springer, Heidelberg (2003)
Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Programming Languages Design and Implementation (PLDI), ACM Sigplan (2003)
Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical report, Compaq Systems Research Center (1998)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Research report, National ICT Australia, Sydney (2004)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: Jml reference manual (draft). Technical report (2004)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, T.: Putting static analysis to work for verification: A case study in issta 2000. Technical report (2000)
Mueller-Olm, M., Seidl, H.: Program analysis through linear algebra. In: 31st Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 330–341 (2004)
Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (1998)
Nipkow, T., Chaieb, A.: Generic proof synthesis for presburger arithmetic – draft. Technical report, Technische Universitaet Muenchen (2004)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Oheimb, D.v.: Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universität München (2001)
Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Proceedings of the 1st Workshop on Bytecode, Bytecode 2005 (2005) (submitted for publication)
Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)
Wildmoser, M., Nipkow, T., Klein, G., Nanz, S.: Prototyping proof carrying code. In: Proc. 3rd IFIP Int. Conf. Theoretical Computer Science, TCS 2004 (2004)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wildmoser, M., Nipkow, T. (2005). Asserting Bytecode Safety. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)