The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining character...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2014
|
| Online Access: | http://hdl.handle.net/1721.1/86042 https://orcid.org/0000-0001-7085-9417 |
| _version_ | 1826212944854122496 |
|---|---|
| author | Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chlipala, Adam |
| author_sort | Chlipala, Adam |
| collection | MIT |
| description | We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack. |
| first_indexed | 2024-09-23T15:40:38Z |
| format | Article |
| id | mit-1721.1/86042 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T15:40:38Z |
| publishDate | 2014 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/860422022-09-29T15:24:31Z The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Chlipala, Adam We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack. United States. Defense Advanced Research Projects Agency (Agreement FA8750-12-2-0293)) 2014-04-07T12:42:35Z 2014-04-07T12:42:35Z 2013-09 Article http://purl.org/eprint/type/JournalArticle 9781450323260 http://hdl.handle.net/1721.1/86042 Adam Chlipala. 2013. The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. SIGPLAN Not. 48, 9 (September 2013), 391-402. https://orcid.org/0000-0001-7085-9417 en_US http://dx.doi.org/10.1145/2500365.2500592 Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (ICFP '13) Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Chlipala, Adam The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title_full | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title_fullStr | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title_full_unstemmed | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title_short | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier |
| title_sort | bedrock structured programming system combining generative metaprogramming and hoare logic in an extensible program verifier |
| url | http://hdl.handle.net/1721.1/86042 https://orcid.org/0000-0001-7085-9417 |
| work_keys_str_mv | AT chlipalaadam thebedrockstructuredprogrammingsystemcombininggenerativemetaprogrammingandhoarelogicinanextensibleprogramverifier AT chlipalaadam bedrockstructuredprogrammingsystemcombininggenerativemetaprogrammingandhoarelogicinanextensibleprogramverifier |