Back to Search
Start Over
A type system for extracting functional specifications from memory-safe imperative programs
- Source :
- Proceedings of the ACM on Programming Languages. 5:1-29
- Publication Year :
- 2021
- Publisher :
- Association for Computing Machinery (ACM), 2021.
-
Abstract
- 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.
- Subjects :
- 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
Subjects
Details
- ISSN :
- 24751421
- Volume :
- 5
- Database :
- OpenAIRE
- Journal :
- Proceedings of the ACM on Programming Languages
- Accession number :
- edsair.doi...........93b798d0b5c5f53267c8b3d9fdefd315