Thesis Details

Instrumentace Java programů, kontrakty pro paralelismus

Master's Thesis Student: Žárský Jan Academic Year: 2020/2021 Supervisor: Smrčka Aleš, Ing., Ph.D.
English title
Parametric Contracts for Concurrency in Java Programs
Language
Czech
Abstract

Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.

Keywords

software verification, dynamic analysis, Java, contracts for concurrency, RoadRunner, instrumentation, Java bytecode, concurrent programming

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology, Field of Study Information Technology Security
Files
Status
defended, grade C
Date
23 June 2021
Reviewer
Křena Bohuslav, Ing., Ph.D.
Committee
Drahanský Martin, prof. Ing., Dipl.-Ing., Ph.D. (DITS FIT BUT), předseda
Hrubý Martin, Ing., Ph.D. (DITS FIT BUT), člen
Malinka Kamil, Mgr., Ph.D. (DITS FIT BUT), člen
Očenášek Pavel, Mgr. Ing., Ph.D. (DIFS FIT BUT), člen
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), člen
Citation
ŽÁRSKÝ, Jan. Instrumentace Java programů, kontrakty pro paralelismus. Brno, 2021. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2021-06-23. Supervised by Smrčka Aleš. Available from: https://www.fit.vut.cz/study/thesis/23103/
BibTeX 
@mastersthesis{FITMT23103,
    author = "Jan \v{Z}\'{a}rsk\'{y}",
    type = "Master's thesis",
    title = "Instrumentace Java program\r{u}, kontrakty pro paralelismus",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2021,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/23103/"
}

Theses

Back to top