A program logic for resources

DOI10.1016/J.TCS.2007.09.003zbMath1133.68010OpenAlexW2159897916MaRDI QIDQ2463560

Alberto Momigliano, Martin Hofmann, Hans-Wolfgang Loidl, Lennart Beringer, David Aspinall

Publication date: 14 December 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/16403450/A_program_logic_for_resources.pdf

zbMATH Keywords

program logiccost modellingobject-oriented languagesJava virtual machine languagelightweight verificationproof-carrying-codequantitative type-systems

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70)

Related Items (11)

Proof optimization for partial redundancy elimination ⋮ Time Bounds for General Function Pointers ⋮ A Hoare Logic for Energy Consumption Analysis ⋮ Reasoning About Resources in the Embedded Systems Language Hume ⋮ A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation ⋮ Recursion Schemata for NC k ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Long-run cost analysis by approximation of linear operators over dioids ⋮ Safety Guarantees from Explicit Resource Management ⋮ Relational Decomposition ⋮ A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation

Uses Software

• Unnamed Item
• KRAKATOA
• Why3
• JML
• Caduceus
• KeY
• KIV
• LOOP
• Grail
• Camelot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic methodology and software technology. 10th international conference, AMAST 2004, Stirling, Scotland, UK, July 12--16, 2004. Proceedings.
• Virginity: A contribution to the specification of object-oriented software
• An assertion-based proof system for multithreaded Java
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Hoare logic and auxiliary variables
• Programming languages and systems. 14th European symposium on programming, ESOP 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings.
• Static prediction of heap space usage for first-order functional programs
• Verification of Array, Record, and Pointer Operations in Pascal
• Soundness and Completeness of an Axiom System for Program Verification
• Hoare logic for Java in Isabelle/HOL
• Bytecode verification on Java smart cards
• Computer Science Logic
• Algebraic Methodology and Software Technology
• Algebraic Methodology and Software Technology
• Fundamental Approaches to Software Engineering
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Logic for Programming, Artificial Intelligence, and Reasoning
• Correct Hardware Design and Verification Methods
• Automated Deduction – CADE-19
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: A program logic for resources