Using Isabelle/HOL to develop and maintain separation invariants for an operating system

H. Blasum, O. Havle, B. Langenstein, Y. Nemouchi, J. Schmaltz, W. Stephan, S. Tverdyshev, F. Verbeek, B. Wolff

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

Samenvatting

We describe work on an Isabelle/HOL model for the specification of a separation kernel done within the EURO-MILS (http://www.euromils.eu/) project. We chose to extensible records to specify the state. By an example of a theory specifying a group of "event" API calls, it is shown how lemmas on local state are used for obtaining proof obligations for a global separation property.
Originele taal-2Engels
TitelIsabelle Workshop (Vienna, Austria, July 13, 2014; part of FLoC)
StatusGepubliceerd - 2014
Evenement2014 Isabelle Workshop, July 13, 2014, Vienna, Austria - Vienna, Oostenrijk
Duur: 13 jul 201413 jul 2014
http://vsl2014.at/isabelle

Congres

Congres2014 Isabelle Workshop, July 13, 2014, Vienna, Austria
Land/RegioOostenrijk
StadVienna
Periode13/07/1413/07/14
Internet adres

Vingerafdruk

Duik in de onderzoeksthema's van 'Using Isabelle/HOL to develop and maintain separation invariants for an operating system'. Samen vormen ze een unieke vingerafdruk.

Citeer dit