@inproceedings{leino2007using,
author = {Leino, Rustan and Schulte, Wolfram},
title = {Using History Invariants to Verify Observers},
series = {Lecture Notes in Computer Science},
booktitle = {ESOP},
year = {2007},
month = {January},
abstract = {This paper contributes a technique that expands the set of object invariants that one can reason about in modular verification. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a flexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem.},
publisher = {Springer},
url = {http://approjects.co.za/?big=en-us/research/publication/using-history-invariants-to-verify-observers/},
pages = {80-94},
volume = {4421},
isbn = {978-3-540-71314-2},
edition = {ESOP},
}