Support for C++ in GMC
Název práce v češtině: | Support for C++ in GMC |
---|---|
Název v anglickém jazyce: | Support for C++ in GMC |
Klíčová slova: | formální verifikace, C++, GMC |
Klíčová slova anglicky: | formal verification, C++, GMC |
Akademický rok vypsání: | 2011/2012 |
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. Jan Kofroň, Ph.D. |
Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
Datum přihlášení: | 07.11.2011 |
Datum zadání: | 07.11.2011 |
Datum potvrzení stud. oddělením: | 07.12.2011 |
Datum a čas obhajoby: | 09.09.2013 00:00 |
Datum odevzdání elektronické podoby: | 29.07.2013 |
Datum odevzdání tištěné podoby: | 02.08.2013 |
Datum proběhlé obhajoby: | 09.09.2013 |
Oponenti: | doc. RNDr. Petr Hnětynka, Ph.D. |
Zásady pro vypracování |
GMC is a software model checker for the C language. It is based on GIMPLE, which is used as the intermediate representation of C programs in GCC. The goal of the thesis is to extend GMC with a basic support for the C++ language, in particular including handling of classes (constructors, destructors, inheritance and virtual methods) and, if it will turn out to be necessary for it, also exceptions. As an optional task, also support for other C++ features, such as templates, will be a welcome contribution. As a part of the thesis, the student should also demonstrate the achieved results on a set of examples showing usability of the solution. |
Seznam odborné literatury |
[1] GIMPLE, http://gcc.gnu.org/onlinedocs/gccint/GIMPLE.html
[2] GCC, http://gcc.gnu.org/ [3] GMC, http://d3s.mff.cuni.cz/~sery/gmc/ [4] Jan Kouba: Memory Representation for Model Checker of C/C++, MSc. thesis, Charles University in Prague, 2010 [5] Ondrej Krc-Jediny: GIMPLE Model Checker, MSc. thesis, Charles University in Prague, 2011 |