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.
|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
|Conference||2014 Isabelle Workshop, July 13, 2014, Vienna, Austria|
|Period||13/07/14 → 13/07/14|
|Other||One of the FLoC Workshops held during 2014 Vienna Summer of logic|