zbMATH — the first resource for mathematics

A program logic for resources. (English) Zbl 1133.68010
Summary: We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. The infrastructure is designed to be used in a Proof-Carrying Code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have predictable resource behaviour.
This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination; it too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics.
The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs.

68N15 Theory of programming languages
03B70 Logic in computer science
Full Text: DOI
[1] Necula, G., (), 106-116
[2] D. Sannella, M. Hofmann, Mobile resource guarantees, EU OpenFET Project. http://www.groups.inf.ed.ac.uk/mrg/, 2002
[3] Aspinall, D.; Gilmore, S.; Hofmann, M.; Sannella, D.; Stark, I., Mobile resource guarantees for smart devices, (), 1-26
[4] MacKenzie, K.; Wolverson, N., Camelot and grail: resource-aware functional programming on the JVM, (), 29-46
[5] Beringer, L.; MacKenzie, K.; Stark, I., Grail: A functional form for imperative mobile code, (), 1-21
[6] Flanagan, C.; Sabry, A.; Duba, B.F.; Felleisen, M., The essence of compiling with continuations, (), 237-247
[7] C. League, V. Trifonov, Z. Shao, Functional Java bytecode, in: Proc. 5th World Conf. on Systemics, Cybernetics, and Informatics, 2001, pp. 1-6. Workshop on Intermediate Representation Engineering for the Java Virtual Machine
[8] Appel, A.W., Compiling with continuations, (1992), Cambridge University Press
[9] Leroy, X., Bytecode verification for Java smart cards, Software practice and experience, 32, 4, 319-340, (2002) · Zbl 1009.68891
[10] K. MacKenzie, N. Wolverson, Camelot and Grail: Compiling a resource-aware functional language for the Java virtual machine, in: TFP’03, Symp on Trends in Functional Languages, Edinburgh, 11-12 September 2003
[11] Hofmann, M., A type system for bounded space and functional in-place update, Nordic journal of computing, 7, 4, 258-289, (2000) · Zbl 0971.68023
[12] Pym, D.-J.; O’Hearn, P.-W.; Yang, H., Possible worlds and resources: the semantics of BI, Theor. comput. sci., 315, 1, 257-305, (2004) · Zbl 1055.03021
[13] Aspinall, D.; Beringer, L.; Momigliano, A., Optimisation validation, Electron. notes theor. comput. sci., 176, 3, 37-59, (2007)
[14] A. Chander, J. Mitchell, I. Shin, Mobile code security by Java bytecode instrumentation, in: DARPA Information Survivability Conference & Exposition, DISCEX II, 2001, pp. 1-15
[15] A. Chander, D. Espinosa, N. Islam, P. Lee, G.C. Necula, Enforcing resource bounds via static verification of dynamic checks, in: Sagiv [81], pp. 311-325 · Zbl 1108.68419
[16] Czajkowski, G.; von Eicken, T., Jres: A resource accounting interface for Java, ACM SIGPLAN notices, 33, 10, 21-35, (1998)
[17] Aspinall, D.; Beringer, L.; Hofmann, M.; Loidl, H.-W.; Momigliano, A., A program logic for resource verification, (), 34-49 · Zbl 1099.68584
[18] Schneider, F.B., Enforceable security policies, ACM transactions on information and system security, 3, 30-50, (2000)
[19] Hoare, C.A.R., An axiomatic basis for computer programming, Communications of the ACM, 12, 10, 576-580, (1969) · Zbl 0179.23105
[20] Jones, C., Systematic software development using VDM, (1990), Prentice Hall · Zbl 0743.68048
[21] T. Kleymann, Hoare logic and VDM: Machine-checked soundness and completeness proofs, Ph.D. Thesis, LFCS, University of Edinburgh, 1999 · Zbl 0978.03026
[22] Poetzsch-Heffter, A.; Müller, P., A programming logic for sequential Java, (), 162-176
[23] Nipkow, T., Hoare logics in isabelle/HOL, (), 341-367 · Zbl 1097.68632
[24] C. Pierik, F.S. de Boer, Modularity and the rule of adaptation, in: Rattray et al. [82], pp. 394-408 · Zbl 1108.68408
[25] Nipkow, T., Hoare logics for recursive procedures and unbounded nondeterminism, (), 103-119 · Zbl 1020.03029
[26] M. Hofmann, Semantik und Verifikation, in: Lecture Notes, TU Darmstadt, 1998
[27] Cook, S.A., Soundness and completeness of an axiom system for program verification, SIAM journal on computing, 7, 1, 70-90, (1978), See corrigendum in SIAM Journal on Computing 10, 612 · Zbl 0374.68009
[28] G.A. Gorelick, A complete axiomatic system for proving assertions about recursive and non-recursive programs, Tech. Rep. 75, University of Toronto, 1975
[29] P. Homeier, Trustworthy tools for trustworthy programs: A mechanically verified verification condition generator for the total correctness of procedures, Ph.D. Thesis, University of California, 1995
[30] Sokołowski, S., Total correctness for procedures, (), 475-483
[31] Hofmann, M.; Loidl, H.-W.; Beringer, L., Certification of quantitative properties of programs, ()
[32] Appel, A.W., Foundational proof-carrying code, (), 247-258
[33] Beringer, L.; Hofmann, M.; Momigliano, A.; Shkaravska, O., Automatic certification of heap consumption, (), 347-362 · Zbl 1108.68374
[34] Hofmann, M.; Jost, S., Static prediction of heap space usage for first-order functional programs, (), 185-197 · Zbl 1321.68180
[35] Hartel, P.H.; Moreau, L., Formalising the safety of Java, the Java virtual machine and Java card, ACM computing surveys, 33, 4, 517-558, (2001)
[36] von Oheimb, D., Hoare logic for Java in isabelle/HOL, Concurrency and computation: practice and experience, 13, 13, 1173-1214, (2001) · Zbl 0997.68019
[37] F. Tang, M. Hofmann, Generating verification conditions for Abadi and Leino’s logic of objects, in: FOOL9 — Ninth International Workshop on Foundations of Object-Oriented Languages, Portland, OR, 2002, pp. 1-11
[38] de Boer, F., A WP-calculus for OO, (), 135-149
[39] Pierik, C.; de Boer, F.S., A syntax-directed Hoare logic for object-oriented programming concepts, (), 64-78 · Zbl 1253.68087
[40] d. Boer, F.; Pierik, C., Computer-aided specification and verification of annotated object-oriented programs, (), 163-177 · Zbl 1048.68050
[41] Á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) · Zbl 1070.68016
[42] Abadi, M.; Leino, R., A logic of object-oriented programs, (), 682-696
[43] Leino, R., Recursive object types in a logic of object-oriented programs, Nordic journal of computing, 5, 4, 330-360, (1998) · Zbl 0913.68025
[44] J. Meyer, P. Müller, A. Poetzsch-Heffter, Programming and interface specification language of JIVE - specification and design rationale, available from citeseer.ist.psu.edu/86897.html, 2000
[45] van den Berg, J.; Jacobs, B., The LOOP compiler for Java and JML, (), 299-315 · Zbl 0978.68708
[46] Huisman, M.; Jacobs, B., Java program verfication via a Hoare logic with abrupt termination, (), 284-303
[47] Jacobs, B.; Poll, E., A logic for the Java modeling language JML, (), 284-299 · Zbl 0977.68588
[48] Marché, C.; Paulin-Mohring, C.; Urbain, X., The \sckrakatoa tool for certification of \scjava/javacard programs annotated in \scjml, Journal of logic and algebraic programming, 58, 1-2, 89-106, (2004) · Zbl 1073.68678
[49] Filliâtre, J.-C.; Marché, C., The why/krakatoa/caduceus platform for deductive program verification, (), 173-177
[50] Burdy, L.; Requet, A.; Lanet, J.-L., Java applet correctness: A developer-oriented approach, (), 422-439
[51] Burdy, L.; Huisman, M.; Pavlova, M., Preliminary design of BML: A behavioral interface specification language for Java bytecode, (), 215-229
[52] Barthe, G.; Pavlova, M.; Schneider, G., Precise analysis of memory consumption using program logics, (), 86-95
[53] Ahrendt, W.; Baar, T.; Beckert, B.; Bubel, R.; Giese, M.; Hähnle, R.; Menzel, W.; Mostowski, W.; Roth, A.; Schlager, S.; Schmitt, P.H., The key tool, Software and systems modeling, 4, 1, 32-54, (2005)
[54] Beckert, B., A dynamic logic for the formal verification of Java card programs, (), 6-24 · Zbl 0980.68525
[55] Mostowski, W., Formalisation and verification of Java card security properties in dynamic logic, (), 357-371 · Zbl 1119.68351
[56] Hähnle, R.; Mostowski, W., Verification of safety properties in the presence of transactions, (), 151-171
[57] Balser, M.; Reif, W.; Schellhorn, G.; Stenzel, K.; Thums, A., Formal system development with KIV, (), 363-366
[58] K. Stenzel, A formally verified calculus for full Java Card, in: Rattray et al. [82], pp. 491-505 · Zbl 1108.68414
[59] Cok, D.R.; Kiniry, J.R., Esc/java2: uniting ESC/Java and JML. progress and issues in building and using ESC/java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system, (), 108-129
[60] Reynolds, J.C., Separation logic: A logic for shared mutable data structures, (), 55-74
[61] Berdine, J.; Calcagno, C.; O’Hearn, P.W., Symbolic execution with separation logic, (), 52-68 · Zbl 1159.68363
[62] Luckham, D.C.; Suzuki, N., Verification of array, record, and pointer operations in Pascal, ACM transactions on programming languages and systems, 1, 2, 226-244, (1979) · Zbl 0452.68014
[63] K.R.M. Leino, Toward reliable modular programs, Ph.D. Thesis, California Institute of Technology, Available as Technical Report Caltech-CS-TR-95-03, 1995
[64] Bornat, R., Proving pointer programs in Hoare logic, (), 102-126 · Zbl 0963.68036
[65] Mehta, F.; Nipkow, T., Proving pointer programs in higher-order logic, (), 121-135 · Zbl 1278.68274
[66] M.J.C. Gordon, Mechanizing programming logics in higher-order logic, in: G.M. Birtwistle, P.A. Subrahmanyam (Eds.), Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), Springer, Banff, Canada, 1988, pp. 387-439
[67] Weber, T., Towards mechanized program verification with separation logic, (), 250-264 · Zbl 1095.68058
[68] Quigley, C.L., A programming logic for Java bytecode programs, (), 41-54
[69] M. Wildmoser, T. Nipkow, Asserting bytecode safety, in: Sagiv [81], pp. 326-341 · Zbl 1108.68432
[70] Bannwart, F.; Müller, P., A program logic for bytecode, Electron. notes theor. comput. sci., 141, 1, 255-273, (2005)
[71] Benton, N., A typed logic for stacks and jumps, Microsoft research, (2004)
[72] Wildmoser, M.; Nipkow, T., Certifying machine code safety: shallow versus deep embedding, (), 305-320 · Zbl 1099.68545
[73] Wildmoser, M.; Chaieb, A.; Nipkow, T., Bytecode analysis for proof carrying code, Electron. notes theor. comput. sci., 141, 1, 19-34, (2005)
[74] Moore, J.S., Inductive assertions and operational semantics, (), 289-303 · Zbl 1179.68089
[75] Moore, J.S., Proving theorems about Java and the JVM with ACL2, NATO science series sub series III computer and systems sciences, 191, 227-290, (2003)
[76] M. Hofmann, H.-W. Loidl, From partial correctness to total correctness, MRG Deliverable D6g, Institut für Informatik, Ludwig-Maximilians Universität, München, March 2005
[77] Skalka, C.; Smith, S.F., History effects and verification, (), 107-128 · Zbl 1116.68381
[78] Beckert, B.; Mostowski, W., A program logic for handling Java card’s transaction mechanism, (), 246-260 · Zbl 1032.68573
[79] K.R.M. Leino, R. Stata, Checking object invariants, Tech. Rep. #1997-007, Digital Systems Research Center, Palo Alto, CA, Palo Alto, USA, 1997 · Zbl 1002.68025
[80] Aspinall, D.; MacKenzie, K., Mobile resource policies, (), 16-36
[81] ()
[82] ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.