Structuring the verification of heap-manipulating programs

DOI10.1145/1706299.1706331zbMath1312.68065OpenAlexW2124461564MaRDI QIDQ5255079

Josh Berdine, Aleksandar Nanevski, Viktor Vafeiadis

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706331

zbMATH Keywords

monadstype theoryHoare logicseparation logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Mtac: A monad for typed tactic programming in Coq, Partiality, State and Dependent Types, A Machine-Checked Framework for Relational Separation Logic

Uses Software

• Coq
• Ynot