Automatic proofs of memory deallocation for a Whiley-to-C Compiler

Autor:	Robi Malik, Mark Utting, Min-Hsien Weng
Rok vydání:	2021
Předmět:	Computer science Programming language Static analysis computer.software_genre Theoretical Computer Science Automated theorem proving Memory leak Hardware and Architecture Code (cryptography) Benchmark (computing) Compiler computer Time complexity Software Invariant (computer science)
Zdroj:	Formal Methods in System Design. 57:429-472
ISSN:	1572-8102 0925-9856
DOI:	10.1007/s10703-021-00378-0
Popis:	This paper describes the design and verification of a copy elimination and memory deallocation scheme for a compiler that translates the verification-friendly programming language Whiley into efficient C code. We use a combination of static analysis and runtime flags to replace array copies with reference assignments when possible. Formal proofs have been carried out, both manually and with the automatic theorem prover Boogie, to show that the generated code satisfies a crucial invariant, which is needed to show the absence of invalid memory access errors and memory leaks. Our benchmark results show that the compiler effectively reduces the time complexity of LZ77 decompression from $$O(n^2)$$ to the theoretically lowest possible level $$O(n\log n)$$ while avoiding all memory leaks.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::91708a1c66ae226475b6d27a39c58faf https://doi.org/10.1007/s10703-021-00378-0 Zobrazit plný text záznamu Full text from SpringerLink