Formal reasoning under cached address translation

DOI10.1007/s10817-019-09539-7zbMath1468.68070OpenAlexW2999427823WikidataQ126318699 ScholiaQ126318699MaRDI QIDQ2209539

Hira Taqdees Syeda, Gerwin Klein

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09539-7

zbMATH Keywords

program verificationARMTLBcached address translationFormal reasoning under cached address translation

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of operating systems (68N25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• seL4
• CertiKOS
• GitHub

Cites Work

• Concerned with the unprivileged: user programs in kernel refinement
• Isabelle/HOL. A proof assistant for higher-order logic
• Physical addressing on real hardware in Isabelle/HOL
• Program verification in the presence of cached address translation
• Deep Specifications and Certified Abstraction Layers
• Types, Maps and Separation Logic
• A Brief Overview of HOL4
• Reasoning about Translation Lookaside Buffers
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
• Unnamed Item

This page was built for publication: Formal reasoning under cached address translation