Reasoning about Translation Lookaside Buffers

DOI10.29007/C2F1MaRDI QIDQ4645755zbMATH OpenOpenAlexFDO

Authors Syeda Hira Taqdees, Gerwin Klein

Publication date 10 January 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/c2f1

zbMATH Keywords

Isabelle/HOLmemory management unitoperating systemsprogram verificationtheorem provingtranslation lookaside buffer

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Recommendations

• Formal reasoning under cached address translation
• scientific article; zbMATH DE number 4039334
• One approach to the specification and verification of translators
• Transducer inference by assembling specific languages
• Storage-to-tree transducers with look-ahead
• Program verification in the presence of cached address translation

Cited in

(3)

• Physical addressing on real hardware in Isabelle/HOL
• Program verification in the presence of cached address translation
• Formal reasoning under cached address translation

Describes a project that uses

Uses Software

• seL4
• Isabelle/HOL
• CertiKOS

This page was built for publication: Reasoning about Translation Lookaside Buffers

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