@inproceedings{e414e176b8d4491cbc5dd65f7cc86967,
title = "Backwards and Forwards with Separation Logic",
abstract = "The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.",
author = "Callum Bannister and Peter H{\"o}fner and Gerwin Klein",
note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",
year = "2018",
doi = "10.1007/978-3-319-94821-8_5",
language = "English",
isbn = "9783319948201",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "68--87",
editor = "Jeremy Avigad and Assia Mahboubi",
booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",
address = "Germany",
}