A program logic for resources
From MaRDI portal
Publication:2463560
Recommendations
Cites work
- A syntax-directed Hoare logic for object-oriented programming concepts.
- A type system for bounded space and functional in-place update
- Algebraic Methodology and Software Technology
- Algebraic Methodology and Software Technology
- Algebraic methodology and software technology. 10th international conference, AMAST 2004, Stirling, Scotland, UK, July 12--16, 2004. Proceedings.
- An assertion-based proof system for multithreaded Java
- An axiomatic basis for computer programming
- Bytecode verification on Java smart cards
- Computer Science Logic
- Fundamental Approaches to Software Engineering
- Grail: a functional form for imperative mobile code
- Hoare logic and auxiliary variables
- Hoare logic for Java in Isabelle/HOL
- scientific article; zbMATH DE number 1612488 (Why is no real title available?)
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- scientific article; zbMATH DE number 1701766 (Why is no real title available?)
- scientific article; zbMATH DE number 1706329 (Why is no real title available?)
- scientific article; zbMATH DE number 46957 (Why is no real title available?)
- scientific article; zbMATH DE number 3562459 (Why is no real title available?)
- scientific article; zbMATH DE number 1251179 (Why is no real title available?)
- scientific article; zbMATH DE number 1948157 (Why is no real title available?)
- scientific article; zbMATH DE number 1956492 (Why is no real title available?)
- scientific article; zbMATH DE number 1860624 (Why is no real title available?)
- scientific article; zbMATH DE number 2110621 (Why is no real title available?)
- Inductive assertions and operational semantics
- Logic for Programming, Artificial Intelligence, and Reasoning
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Programming Languages and Systems
- Programming Languages and Systems
- Programming Languages and Systems
- Programming Languages and Systems
- 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.
- Proving pointer programs in higher-order logic.
- Soundness and Completeness of an Axiom System for Program Verification
- Static prediction of heap space usage for first-order functional programs
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Verification of Array, Record, and Pointer Operations in Pascal
- Virginity: A contribution to the specification of object-oriented software
Cited in
(15)- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation
- Relational decomposition
- Time bounds for general function pointers
- A Hoare logic for energy consumption analysis
- Reasoning about resources in the embedded systems language Hume
- Recursion Schemata for NC k
- Long-run cost analysis by approximation of linear operators over dioids
- Safety Guarantees from Explicit Resource Management
- A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
- A Bytecode Logic for JML and Types
- Theorem Proving in Higher Order Logics
- Logic for Programming, Artificial Intelligence, and Reasoning
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Quantitative static analysis over semirings: analysing cache behaviour for Java Card
- Proof optimization for partial redundancy elimination
Describes a project that uses
Uses Software
This page was built for publication: A program logic for resources
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2463560)
