Soothsharp: A C#-to-Viper translator
| Název práce v češtině: | Soothsharp: překladač C# do jazyka Viper |
|---|---|
| Název v anglickém jazyce: | Soothsharp: A C#-to-Viper translator |
| Klíčová slova: | verifikace, programovací jazyky, kontrakty, oprávnění |
| Klíčová slova anglicky: | verification, programming languages, contracts, permissions |
| Akademický rok vypsání: | 2016/2017 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Pavel Parízek, Ph.D. |
| Řešitel: | Mgr. Petr Hudeček - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 12.10.2016 |
| Datum zadání: | 13.10.2016 |
| Datum potvrzení stud. oddělením: | 15.11.2016 |
| Datum a čas obhajoby: | 06.09.2017 10:00 |
| Datum odevzdání elektronické podoby: | 28.06.2017 |
| Datum odevzdání tištěné podoby: | 21.07.2017 |
| Datum proběhlé obhajoby: | 06.09.2017 |
| Oponenti: | Mgr. Pavel Ježek, Ph.D. |
| Zásady pro vypracování |
| A very popular approach to verification of object-oriented programs is through annotation of individual methods with contracts (preconditions, postconditions, invariants) and subsequent translation into a program in an intermediate language of some kind, which is then verified using a dedicated tool.
The objective of this thesis is to create such a transcompiler that will take a program in C# and produce equivalent source code in the Viper intermediate verification language, which is developed at ETH Zurich as a part of the Viper project. This will permit methods in the C# program to be formally analyzed for correctness with respect to their contracts. The candidate will implement a standalone application, a Visual Studio plugin, and a set of test cases. The C# language will not be supported in its entirety, and only a minimal number of BCL classes will be translated. However, the transcompiler should at least support all control structures, basic object-oriented programming, most features of the Viper language, and arrays. |
| Seznam odborné literatury |
| 1. Viper toolset. http://www.pm.inf.ethz.ch/research/viper.html
2. P. Mueller, M. Schwerhoff, and A.J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. VMCAI 2016, LNCS 9583. 3. B. Brodowsky. Translating Scala to SIL. Master Thesis, ETH Zurich, 2012 |