Why Just Boogie? Translating Between Intermediate Verification Languages
Abstract
The verification systems Boogie and Why3 use their respective intermediate languages to generate verification conditions from high-level programs. Since the two systems support different back-end provers (such as Z3 and Alt-Ergo) and are used to encode different high-level languages (such as C# and Java), being able to translate between their intermediate languages would provide a way to reuse one system's features to verify programs meant for the other. This paper describes a translation of Boogie into WhyML (Why3's intermediate language) that preserves semantics, verifiability, and program structure to a large degree. We implemented the translation as a tool and applied it to 194 Boogie-verified programs of various sources and sizes; Why3 verified 83% of the translated programs with the same outcome as Boogie. These results indicate that the translation is often effective and practically applicable.
Cite
@article{arxiv.1601.00516,
title = {Why Just Boogie? Translating Between Intermediate Verification Languages},
author = {Michael Ameri and Carlo A. Furia},
journal= {arXiv preprint arXiv:1601.00516},
year = {2016}
}