@inproceedings{86e6cc4919b4477c966aec4dfccfbfd7,
title = "Being and Change: Reasoning About Invariance",
abstract = "We introduce a new way of reasoning about invariance in terms of foot-prints in a Hoare logic for recursive programs with (unbounded) arrays. A foot-print of a statement is a predicate that describes that part of the state that can be changed by the statement. We define invariance of an assertion with respect to a foot-print by means of a logical operation. This new Hoare logic is applied in a new simpler and modular proof of correctness of the well-known Quicksort sorting algorithm.",
author = "Boer, {Frank S. de} and Gouw, {Stijn de}",
year = "2015",
doi = "10.1007/978-3-319-23506-6_13",
language = "English",
isbn = "978-3-319-23505-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "191--204",
editor = "{Roland Meyer} and {Andr{\'e} Platzer} and {Heike Wehrheim}",
booktitle = "Correct System Design",
edition = "1",
}