The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
CVM – A Verified Framework for Microkernel Programmers
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
CVM (communicating virtual machines) is a computational model for concurrent user processes interacting with a generic microkernel—supporting virtual memory—and devices. In this paper, we introduce the computational models needed to define CVM. Furthermore, we describe how CVM can be implemented by means of a concrete kernel, thus providing a trustworthy platform for microkernel programmers. Last but not least, we give an overview on the model formalization and implementation correctness proof, which has been conducted in the interactive theorem prover Isabelle for the most part. An endeavor like this is tedious and of a considerable complexity. Thus, we do not try to present all details, but provide references to publications covering specific aspects.
@article{derrieden2008cvm,
title = {CVM – A Verified Framework for Microkernel Programmers},
author = {Tom In der Rieden and Alexandra Tsyban},
year = {2008},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier BV},
volume = {217},
pages = {151--168},
doi = {10.1016/j.entcs.2008.06.047},
}