Time credits and time receipts in Iris

DOI10.1007/978-3-030-17184-1_1MaRDI QIDQ6091293zbMATH OpenOpenAlexFDO

Authors Glen Mével, Jacques-Henri Jourdan, François Pottier

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17184-1_1

zbMATH Keywords

Irisprogram logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Hoare logics for time bounds. A study in meta theory
• Time bounds for general function pointers
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• scientific article; zbMATH DE number 3846835
• A Hoare-like proof system for analysing the computation time of programs

Cited in

(2)

• Inductive predicates via least fixpoints in higher-order separation logic
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)

This page was built for publication: Time credits and time receipts in Iris

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