A program logic for resources
From MaRDI portal
Publication:2463560
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
program logiccost modellingobject-oriented languagesJava virtual machine languagelightweight verificationproof-carrying-codequantitative type-systems
Related Items
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
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
