Verifikace ukazatelových programů pomocí lesních automatů

English title

Verification of Pointer Programs Based on Forest Automata

Language

Czech

Abstract

In this work, we focus on improving the forest automata based shape analysis implemented in the Forester tool. This approach represents shapes of the heap using forest automata. Forest automata are based on tree automata and Forester currently has only a simple implementation of tree automata. Our first contribution is replacing this implementation by the general purpose tree automata library VATA, which contains the highly optimized implementations of automata operations. The version of Forester using the VATA library participated in the competition SV-COMP 2015. We further extended the forest automata based verification method with two new techniques - a counterexample analysis and predicate abstraction. The first one allows us to determine whether a found error is a real or spurious one. The results of the counterexample analysis is also used for creating new predicates which are used for the refinement of predicate abstraction. We show that both of these techniques contribute to an improvement over the early approach.

Keywords

lesní automaty, formální verifikace, statická analýza, složité datové struktury, stromové automaty, zpětný běh, predikátová abstrakce.

Department

Department of Intelligent Systems FIT BUT

Degree Programme

Information Technology, Field of Study Mathematical Methods in Information Technology

Files

Thesis text 651 kB

Status

defended, grade A

Date

24 June 2015

Reviewer

Rogalewicz Adam, doc. Mgr., Ph.D.

Committee

Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Burget Radek, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Drahanský Martin, prof. Ing., Dipl.-Ing., Ph.D. (DITS FIT BUT), člen
Hrubý Martin, Ing., Ph.D. (DITS FIT BUT), člen
Rozinajová Viera, doc. Ing., Ph.D. (FIIT STU), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen

Citation

HRUŠKA, Martin. Verifikace ukazatelových programů pomocí lesních automatů. Brno, 2015. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2015-06-24. Supervised by Holík Lukáš. Available from: https://www.fit.vut.cz/study/thesis/17838/

BibTeX

@mastersthesis{FITMT17838,
    author = "Martin Hru\v{s}ka",
    type = "Master's thesis",
    title = "Verifikace ukazatelov\'{y}ch program\r{u} pomoc\'{i} lesn\'{i}ch automat\r{u}",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2015,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/17838/"
}