Reasoning About Resources in the Embedded Systems Language Hume

DOI10.1007/978-3-319-12466-7_7zbMath1445.68044OpenAlexW1004448426MaRDI QIDQ3460507

Gudmund Grov, Hans-Wolfgang Loidl

Publication date: 7 January 2016

Published in: Foundational and Practical Aspects of Resource Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-12466-7_7

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A brief history of process algebra
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Hoare logic and auxiliary variables
• CSP theorems for communicating B machines
• A program logic for resources
• Hoare logic for Java in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• csp2B: A practical approach to combining CSP and B

This page was built for publication: Reasoning About Resources in the Embedded Systems Language Hume