Viper is a verification infrastructure developed at ETH Zurich. Using this infrastructure, programs written in the Viper language may be analyzed for correctness with respect to assertions and contracts. In this thesis, we develop a contracts library and a translator program that compiles C# code into the Viper language and thus allows it to be verified. A user may annotate their C# program with these contracts and then use the translator to determine its functional correctness. The translator supports most C# features, including types and arrays. It also integrates with Visual Studio, showing translation and verification errors to the user on-the-fly.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:364940 |
| Date | January 2017 |
| Creators | Hudeček, Petr |
| Contributors | Parízek, Pavel, Ježek, Pavel |
| Source Sets | Czech ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0014 seconds