Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 368)
Detail práce
   Přihlásit přes CAS
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
 
Univerzita Karlova | Informační systém UK