Soothsharp: A C#-to-Viper translator
| Thesis title in Czech: | Soothsharp: překladač C# do jazyka Viper |
|---|---|
| Thesis title in English: | Soothsharp: A C#-to-Viper translator |
| Key words: | verifikace, programovací jazyky, kontrakty, oprávnění |
| English key words: | verification, programming languages, contracts, permissions |
| Academic year of topic announcement: | 2016/2017 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Pavel Parízek, Ph.D. |
| Author: | Mgr. Petr Hudeček - assigned and confirmed by the Study Dept. |
| Date of registration: | 12.10.2016 |
| Date of assignment: | 13.10.2016 |
| Confirmed by Study dept. on: | 15.11.2016 |
| Date and time of defence: | 06.09.2017 10:00 |
| Date of electronic submission: | 28.06.2017 |
| Date of submission of printed version: | 21.07.2017 |
| Date of proceeded defence: | 06.09.2017 |
| Opponents: | Mgr. Pavel Ježek, Ph.D. |
| Guidelines |
| 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. |
| References |
| 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 |