Abstract / Description of output
The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent. This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying.
Original language | English |
---|---|
Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation. Modeling |
Subtitle of host publication | 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I |
Editors | Tiziana Margaria, Bernhard Steffen |
Place of Publication | Cham |
Publisher | Springer |
Pages | 134-149 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-030-03418-4 |
ISBN (Print) | 978-3-030-03417-7 |
DOIs | |
Publication status | Published - 29 Oct 2018 |
Event | 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - Limassol, Cyprus Duration: 30 Oct 2018 → 13 Nov 2018 http://www.isola-conference.org/isola2018/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer, Cham |
Volume | 11244 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation |
---|---|
Abbreviated title | ISoLA 2018 |
Country/Territory | Cyprus |
City | Limassol |
Period | 30/10/18 → 13/11/18 |
Internet address |