Skip to main content
Conference Proceedings

Mechanising data-types for kernel design in z

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2009) 5902 LNCS 186-203
DOI: 10.1007/978-3-642-10452-7_13
4Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present results from the mechanisation of a priority queue and its operations. Our interest comes from its use in the specification and refinement of a scheduler for OS kernels for embedded real-time devices. It is part of a pilot project within the international Grand Challenge in Verified Software. Our work uncovers important hidden and missing properties, and their relation to kernel design. © 2009 Springer-Verlag Berlin Heidelberg.

Cite

CITATION STYLE

APA

Freitas, L. (2009). Mechanising data-types for kernel design in z. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5902 LNCS, pp. 186–203). https://doi.org/10.1007/978-3-642-10452-7_13

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free