Original title:
GIMPLE Model Checker
Translated title:
GIMPLE Model Checker
Authors:
Krč-Jediný, Ondrej ; Šerý, Ondřej (advisor) ; Hauzar, David (referee) Document type: Master’s theses
Year:
2011
Language:
eng Abstract:
[eng][cze] Title: GIMPLE Model Checker Author: Ondrej Krč-Jediný Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Ondřej Šerý Ph.D. Supervisor's e-mail address: Ondrej.Sery@mff.cuni.cz The goal of the thesis is a prototype implementation of explicit-state model checker of C - an advanced tool for finding errors in programs. This tool ex- plores all possible paths of program execution as well as all thread interleavings. It is based on GIMPLE - output of front-end of GCC compiler, which is the input language for GMC. The thesis is based on the previous work 'Memory represen- tation for GIMPLE Model Checker', that implements work with memory for this tool. Since it is based on GIMPLE, it makes it possible to verify systems directly in C. In addition, it is easily extensible to other languages supported by GCC. Keywords: model checking, GIMPLE, GCC, C 1Název práce: GIMPLE Model Checker Autor: Ondrej Krč-Jediný Katedra (ústav): Katedra distribuovaných a spolehlivých systémů Vedoucí diplomové práce: RNDr. Ondřej Šerý Ph.D. e-mail vedoucího: Ondrej.Sery@mff.cuni.cz Abstrakt: Cieľom práce je implementácia základných prvkov explicit-state model checkeru pre jazyk C - pokročilého nástroja na hľadanie chýb v programoch. Tento nástroj prehľadáva všetky možné cesty, ktorými môže byť program vykonávaný a zároveň vyskúša všetky možné kombinácie prekladania vlákien. Nástroj je založený na GIMPLE - výstupe front-endu kompilátora GCC, ktorý berie za svoj vstupný jazyk. Práca využíva predchádzajúcu prácu 'Memory representa- tion for GIMPLE Model Checker', ktorá implementuje prácu s pamäťou pre tento nástroj. Tým, že je nástroj vychádza z GIMPLE, umožňuje overovanie systémov priamo v jazyku C, naviac je ľahko rozšíriteľný na iné jazyky podporované GCC. 1
Keywords:
C; GCC; GIMPLE; model checking; C; GCC; GIMPLE; model checking
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/33398