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

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

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Isabelle Workshop (Vienna, Austria, July 13, 2014; part of FLoC)
Publication status	Published - 2014
Event	2014 Isabelle Workshop, July 13, 2014, Vienna, Austria - Vienna, Austria Duration: 13 Jul 2014 → 13 Jul 2014 http://vsl2014.at/isabelle

Conference

Conference	2014 Isabelle Workshop, July 13, 2014, Vienna, Austria
Country/Territory	Austria
City	Vienna
Period	13/07/14 → 13/07/14
Other	One of the FLoC Workshops held during 2014 Vienna Summer of logic
Internet address	http://vsl2014.at/isabelle

Cite this

@inproceedings{96da6c42df8a4e23a4060d8f7318cdfc,

title = "Using Isabelle/HOL to develop and maintain separation invariants for an operating system",

abstract = "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.",

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

year = "2014",

language = "English",

booktitle = "Isabelle Workshop (Vienna, Austria, July 13, 2014; part of FLoC)",

note = "2014 Isabelle Workshop, July 13, 2014, Vienna, Austria ; Conference date: 13-07-2014 Through 13-07-2014",

url = " http://vsl2014.at/isabelle",

}

TY - GEN

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

AU - Blasum, H.

AU - Havle, O.

AU - Langenstein, B.

AU - Nemouchi, Y.

AU - Schmaltz, J.

AU - Stephan, W.

AU - Tverdyshev, S.

AU - Verbeek, F.

AU - Wolff, B.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

M3 - Conference contribution

BT - Isabelle Workshop (Vienna, Austria, July 13, 2014; part of FLoC)

T2 - 2014 Isabelle Workshop, July 13, 2014, Vienna, Austria

Y2 - 13 July 2014 through 13 July 2014

ER -

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

Abstract

Conference

Fingerprint

Cite this