CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Why Just Boogie? Translating Between Intermediate Verification Languages

M. Ameri ; Carlo A. Furia (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Integrated Formal Methods (0302-9743). Vol. 9681 (2016), p. 79-95.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: formal verification

Denna post skapades 2016-08-23.
CPL Pubid: 240633


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)



Chalmers infrastruktur