Original title: Soothsharp: překladač C# do jazyka Viper
Translated title: Soothsharp: A C#-to-Viper translator
Authors: Hudeček, Petr ; Parízek, Pavel (advisor) ; Ježek, Pavel (referee)
Document type: Master’s theses
Year: 2017
Language: eng
Abstract: [eng] [cze]
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. Viper je verifikační infrastruktura vyvíjená na univerzitě ETH v Curychu. Pomocí této infrastruktury se dá ověřit, zda programy napsané v jazyku Viper vyhovují svým deklarovaným kontraktům a invariantům. V této práci vyvíjíme knihovnu kontraktů a překladač, který zkompiluje kód v jazyku C# do jazyku Viper, a tak umožní jeho verifikaci. Uživatel může anotovat svůj program těmito kontrakty a pak použít překladač, aby určil, zda je program funkčně korektní. Překladač podporuje podstatnou podmnožinu funkcí jayzku C#, včetně typů a polí. Je integrován s Visual Studiem, a ukazuje tak chyby z překladu a verifikace uživateli přímo v prostředí.
Keywords: contracts; permissions; programming languages; verification; kontrakty; oprávnění; programovací jazyky; verifikace

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/90340

Permalink: http://www.nusl.cz/ntk/nusl-364940


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses