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

DOI10.1007/s10703-021-00378-0OpenAlexW3195123533WikidataQ113902719 ScholiaQ113902719MaRDI QIDQ2058392

Min-Hsien Weng, Robi Malik, Mark Utting

Publication date: 8 December 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00378-0

zbMATH Keywords

program verificationcompilercall by valuememory deallocation

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Valgrind
• Boogie
• Gprof
• Whiley

Cites Work

• Unnamed Item
• Boogie
• Set constraints for destructive array update optimization
• Dependent types and multi-monadic effects in F*
• A universal algorithm for sequential data compression
• Logic in Computer Science
• Compiler Design

This page was built for publication: Automatic proofs of memory deallocation for a Whiley-to-C compiler