Název: Support for C++ in GMC
Překlad názvu: Support for C++ in GMC
Autoři: Šebetovský, Jan ; Kofroň, Jan (vedoucí práce) ; Hnětynka, Petr (oponent)
Typ dokumentu: Diplomové práce
Rok: 2013
Jazyk: eng
Abstrakt: [eng] [cze]
Software is used in more and more aspects of our lives, so its correctness is more and more important. Its verification is thus a good idea. Now there are not many tools for verification of programs in the C++ language and most of them cannot verify all required properties. Because of this we decided to extend GMC, which was already able to verify C code, with support of the C++ language. However the C++ language is very vast, so the goal of this work is implementation of only the basic language features (inheritance, constructors, destructors, virtual methods and exceptions). The support of all those features have been implemented except for exceptions, which are implemented only partially. Powered by TCPDF (www.tcpdf.org) Software je používán na stále více místech našeho života a tak je stále důležitější jeho správnost. Proto je dobré přistoupit k jeho formální verifikaci. V současnosti neexistuje mnoho nástrojů pro verifikaci kódu v jazyce C++ a většina z nich neumí verifikovat všechny potřebné vlastnosti. Proto jsme se rozhodli rozšířit program GMC, který už uměl kontrolovat programy v jazyce C, o podporu jazyka C++. Kvůli značné rozsáhlosti jazyka C++ bylo cílem této práce implementovat jen základní vlastnosti jazyka (dědičnost, konstruktory, destruktory, virtuální metody a výjimky). Podpora všech těchto vlastností byla implementována až na výjimky, které jsou implementovány jen částečně. Powered by TCPDF (www.tcpdf.org)
Klíčová slova: C++; formální verifikace; GMC; C++; formal verification; GMC

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/59000

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-328250


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce