Verification Condition Generation and Variable Conditions in Smallfoot
Logic in Computer Science
2012-04-24 v1 Programming Languages
Abstract
These notes are a companion to [1] which describe - the variable conditions that Smallfoot checks, - the analysis used to check them, - the algorithm used to compute a set of verification conditions corresponding to an annotated program, and - the treatment of concurrent resource initialization code.
Keywords
Cite
@article{arxiv.1204.4804,
title = {Verification Condition Generation and Variable Conditions in Smallfoot},
author = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
journal= {arXiv preprint arXiv:1204.4804},
year = {2012}
}