A program logic for resource verification

DOI10.1007/978-3-540-30142-4_3MaRDI QIDQ5464660zbMATH OpenOpenAlexFDO

Authors Lennart Beringer, Martin Hofmann, Alberto Momigliano, D. Aspinall, Hans Wolfgang Loidl

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A program logic for resources
• Reasoning about resources in the embedded systems language Hume
• Logic for Programming, Artificial Intelligence, and Reasoning
• Formal Certification of a Resource-Aware Language Implementation
• Amortised resource analysis with separation logic

Cited in

(11)

• A program logic for resources
• Grail: a functional form for imperative mobile code
• A framework for verification and debugging of resource usage properties: resource usage verification
• Formal Certification of a Resource-Aware Language Implementation
• Reasoning about resources in the embedded systems language Hume
• Amortised resource analysis with separation logic
• Certification Using the Mobius Base Logic
• Verification logic
• Complexity verification using guided theorem enumeration
• Programming Languages and Systems
• Logic for Programming, Artificial Intelligence, and Reasoning

Describes a project that uses

Uses Software

• Isabelle/HOL
• KRAKATOA
• Grail

This page was built for publication: A program logic for resource verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5464660)