Abstract
We present a program logic for virtual machine code that may serve as a suitable target for different proof-transforming compilers. Compilation from JML-specified source code is supported by the inclusion of annotations whose interpretation extends to non-terminating computations. Compilation from functional languages, and the communication of results from intermediate level program analysis phases are facilitated by a new judgement format that admits the compositionality of type systems to be reflected in derivations. This makes the logic well suited to serve as a language in which proofs of a PCC architecture are expressed. We substantiate this claim by presenting the compositional encoding of a type system for bounded heap consumption. Both the soundness proof of the logic and the derivation of the type system have been formally verified by an implementation in Isabelle/HOL.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Ábrahám, E., de Boer, F.S., de Roever, W.P., Steffen, M.: An assertion-based proof system for multithreaded Java. Theoretical Computer Science 331(2-3), 251–290 (2005)
Nanevski, L.B.A., Morrisett, G.: Polymorphism and Separation in Hoare Type Theory. In: Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006). ACM Press, New York (2006)
Appel, A.W.: SSA is functional programming. ACM SIGPLAN Notices 33(4), 17–20 (1998)
Appel, A.W.: Foundational proof-carrying code. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos (2001)
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 34–49. Springer, Heidelberg (2004)
Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. In: Knoop, J., Necula, G.C., Zimmermann, W. (eds.) Proceedings of the 5th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006). ENTCS. Elsevier, Amsterdam (to appear, 2006)
Bannwart, F.Y., Müller, P.: A logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE). ENTCS, vol. 141(1), pp. 255–273. Elsevier, Amsterdam (2005)
Barthe, G.: Mobius – Mobility, Ubiquity and Security, http://mobius.inria.fr
Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 626–641. Springer, Heidelberg (2001)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, pp. 14–25. ACM, New York (2004)
Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 364–380. Springer, Heidelberg (2005)
Beringer, L., Hofmann, M.: A bytecode logic for JML and types – Isabelle/HOL sources (2006), http://www.tcs.ifi.lmu.de/~beringer/BytecodeLogic.tar.gz
Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 347–362. Springer, Heidelberg (2005)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Cachera, D., Jensen, T.P., Pichardie, D., Schneider, G.: Certified memory usage analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 91–106. Springer, Heidelberg (2005)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS) 13(4) (October 1991)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002: Proceedings of the ACM Conference on Programming language design and implementation, pp. 234–245. ACM Press, New York (2002)
Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI 1993: Proceedings of the ACM Conference on Programming language design and implementation, pp. 237–247. ACM Press, New York (1993)
Hähnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 151–171. Springer, Heidelberg (2005)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: POPL 2003: Proceedings of the 30th ACM Symposium on Principles of programming languages, pp. 185–197. ACM Press, New York (2003)
Jacobs, B., Poll, E.: A logic for the java modeling language JML. In: Hußmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)
Kelsey, R.A.: A correspondence between continuation passing style and static single assignment form. ACM SIGPLAN Notices 30(3), 13–22 (1995)
Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1998)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J.: JML Reference Manual (draft) (May 2006), http://www.cs.iastate.edu/~leavens/JML
Leino, K.R.M., Stata, R.: Checking object invariants. Technical Report #1997-007, Digital Equipment Corporation Systems Research Center, Palo Alto, USA (1997)
Nanevski, A., Morrisett, G.: Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University (2005)
Necula, G.C.: Proof-carrying code. In: POPL 1997: Proceedings of the 24th ACM Symposium on Principles of programming languages, pp. 106–119. ACM Press, New York (1997)
Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 103–119. Springer, Heidelberg (2002)
Pichardie, D.: Bicolano – Byte Code Language in Coq (2006), http://www-sop.inria.fr/everest/personnel/David.Pichardie/bicolano/main.html
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002)., pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the FLoC Workshop on Run-Time Result Verification (July 1999)
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
Beringer, L., Hofmann, M. (2006). A Bytecode Logic for JML and Types. In: Kobayashi, N. (eds) Programming Languages and Systems. APLAS 2006. Lecture Notes in Computer Science, vol 4279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11924661_24
Download citation
DOI: https://doi.org/10.1007/11924661_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48937-5
Online ISBN: 978-3-540-48938-2
eBook Packages: Computer ScienceComputer Science (R0)