A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code | Zendy

Hendrik Tews | Zendy; Tjark Weber | Zendy; Marcus Völp | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code

Author(s) -

Hendrik Tews,

Tjark Weber,

Marcus Völp

Publication year - 2008

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2008.06.043

Subject(s) - computer science , hypervisor , automated theorem proving , programming language , proof assistant , code (set theory) , formal verification , model checking , high level verification , virtual machine , simple (philosophy) , functional verification , embedded system , operating system , software , mathematical proof , virtualization , software system , software construction , cloud computing , philosophy , geometry , mathematics , set (abstract data type) , epistemology

This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research