"Completeness of Hoare logic with inputs over the standard model."

Zhaowei Xu, Yuefei Sui, Wenhui Zhang (2016)
a service of Schloss Dagstuhl - Leibniz Center for Informatics