-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpapers.tex
91 lines (57 loc) · 4.83 KB
/
papers.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
\ifthesis In this appendix,\else Here\fi{} I summarize my publication results in the field of program analysis.
For my most important papers, I also include a short description of the paper and a description of my contribution to the paper.
The remainder of papers are mostly either older papers to which I have contributed less or short report papers for the Software Verification Competition (SV-COMP\ifthesis~\mcite{Beyer2020svc}\fi).
\section{Most Significant Papers}
\newcommand{\prc}[1]{\hfill{}#1\,\%}
\newcommand{\contrib}{\emph{My Contribution}:\xspace}
\subsection*{Local Nontermination Detection for Parallel C++ Programs}
In this paper, we present our approach to ensuring that parallel programs do not hang or wait indefinitely – i.e., there are no deadlocks, livelocks, and the program proceeds towards its goals.
The paper contains the theoretical description of our approach and evaluation of our publicly available implementation.
\contrib The algorithm design, implementation and writing of the paper was done by me, my advisor Jiří Barnat helped by consulting the theory with me and proofreading the paper.
I have presented this paper on the SEFM 2019 conference.
\prc{90}
\bigskip\noindent\fcite{SB2019}
\subsection*{Model Checking of C++ Programs Under the x86-TSO Memory Model}
Here we present a novel approach to verification of parallel programs with respect to the memory model of Intel processors.
The approach improves the efficiency of explicit-state model checking by decreasing amount of nondeterminism in the program.
The paper contains evaluation and is accompanied by a publicly available implementation.
\contrib The algorithm design, implementation and writing of the paper was done by me, Jiří Barnat helped by consulting the theory with me and proofreading the paper.
I have presented this paper on the ICFEM 2018 conference.
\prc{90}
\bigskip\noindent\fcite{SB2018x86tso}
\subsection*{Using Off-the-Shelf Exception Support Components in C++ Verification}
In this paper, we present an extension of DIVINE that allows it to verify programs that contain C++ exceptions and C programs with a non-local transfer of control flow (\texttt{setjmp}/\texttt{longjmp}).
We show that with careful design, we can successfully reuse exception handling code from the standard C++ library.
The result is that virtually any exception handling constructs working in the standard C++ are now available in DIVINE.
\contrib I have designed the exception support for DIVINE 4, implemented it and performed the evaluation for this paper.
I have also written most of the text for the paper.
Petr Ročkai and Jiří Barnat helped by consulting the design and implementation and also helped with the paper text.
I have presented this paper on the QRS 2017 conference.
The paper and its presentation were awarded the best paper award.
\prc{75}
\bigskip\noindent\fcite{SRB2017}
\subsection*{Model Checking of C and C++ with DIVINE 4}
In this tool paper, we describe the overall architecture of DIVINE 4 and changes in the tool compared to DIVINE 3.
Most significantly, this paper describes the modular nature of DIVINE: DIVINE 4 is built around an efficient interpreter which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of real-world code written in C and C++.
\contrib The text of the paper is written mostly by me, with additions and proofreading by Petr Ročkai and Jiří Barnat.
The architecture design was mostly due to Petr Ročkai, with additions by me and Jan Mrázek.
The implementation includes code by all the co-authors with most significant contributions by (in the order of significance) Petr Ročkai, me, and Jan Mrázek.
\prc{30}
\bigskip\noindent\fcite{DIVINEToolPaper2017}
\subsection*{DiVM: Model Checking with LLVM and Graph Memory}
This paper introduces the concept of a virtual machine with graph memory as a core component for explicit-state and abstraction-based verification of software.
The paper is accompanied by an implementation of the virtual machine which runs LLVM IR (which can be obtained from C or C++ using the clang compiler) and an evaluation which compares the new approach to a more traditional design of an LLVM-based model checker as well as a symbolic model checker.
\contrib The primary author of this paper is Petr Ročkai.
My contribution concerned mostly the C++ support (including program compilation and libraries) and the evaluation and comparison of the new approach with DIVINE 3 and ESBMC.
\prc{20}
\bigskip\noindent\fcite{RSCB2018}
\section{Other Papers}
\bigskip\noindent\fcite{LSRB2019}
\bigskip\noindent\fcite{MJSLB2017}
\bigskip\noindent\fcite{SRB16SVC}
\bigskip\noindent\fcite{BCRSZ16Prob}
\bigskip\noindent\fcite{SRB15weakmem}
\bigskip\noindent\fcite{BRSW15HS}
\bigskip\noindent\fcite{RSB15TC}
\bigskip\noindent\fcite{SRB14CSDR}
\bigskip\noindent\fcite{BBH+13DIVINE}