A type system for extracting functional specifications from memory-safe imperative programs
| Autor: | Adam Wick, Matthew Yacavone, Paul He, Aaron Tomb, Chris Phifer, Steve Zdancewic, Karl Smeltzer, Andrei Ştefănescu, Eddy Westbrook, Valentin Robert, Brent Carmer |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Functional specification
Programming language Computer science 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Index (publishing) 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Key (cryptography) Array data structure Purely functional State (computer science) Safety Risk Reliability and Quality computer Memory safety Software |
| Zdroj: | Proceedings of the ACM on Programming Languages. 5:1-29 |
| ISSN: | 2475-1421 |
| Popis: | Verifying imperative programs is hard. A key difficulty is that the specification of what an imperative program does is often intertwined with details about pointers and imperative state. Although there are a number of powerful separation logics that allow the details of imperative state to be captured and managed, these details are complicated and reasoning about them requires significant time and expertise. In this paper, we take a different approach: a memory-safe type system that, as part of type-checking, extracts functional specifications from imperative programs. This disentangles imperative state, which is handled by the type system, from functional specifications, which can be verified without reference to pointers. A key difficulty is that sometimes memory safety depends crucially on the functional specification of a program; e.g., an array index is only memory-safe if the index is in bounds. To handle this case, our specification extraction inserts dynamic checks into the specification. Verification then requires the additional proof that none of these checks fail. However, these checks are in a purely functional language, and so this proof also requires no reasoning about pointers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|