Annex 6: Habilitation thesis reader’s report
Applicant: Dr. Jiří Barnat, Ph.D.
Reader: Dr. Gerard J. Holzmann
Report
I have read Dr. Barnat’s habilitation’s thesis and evaluated the work that is reported.
There are two main parts to the thesis. The first part, pages 1-18, provide an overview and introduction
to the work that is reported on (p. 1-12), and outlines the main contributions made (p. 13-18). It is
followed by a biography (p. 19-30). The second part of the thesis, covering pages 31-244, contains
reprints of a total of 19 research papers authored or co-authored by Dr. Barnat since the completion of
his PhD work in 2004.
One obstacle in this evaluation is that the majority of the papers included have appeared in conference
proceedings only and not in archival journals, which generally follow a more thorough and reliable peer
review process. Only two of the papers have appeared in traditional journals [12],[27]. The best way to
evaluate or demonstrate the quality of a research contribution in an academic environment is to show
that it can pass the more rigorous peer review process of an archival journal. Without this measure it
becomes more difficult to do a thorough evaluation of the published work. Within the context of this
evaluation it is not possible to perform a journal-standard review of each paper that is included in the
habilitation’s thesis.
Among the conferences where Dr. Barnat’s work has appeared, CAV and TACAS are generally recognized
as among the leading conferences in this domain (as evidenced by their acceptance rates). Two of Dr.
Barnat’s papers have been accepted at CAV conferences (one as a tool paper), and one at a TACAS
conference.
All of Dr. Barnat’s papers list co-authors, which is a positive characteristic of the work (providing the
desirable characteristic of team work), but this also makes it a little harder for an outside evaluator to
determine what the research contribution of the different authors to each paper was. Fortunately, Dr.
Barnat’s contributions do become evident from the totality of the published work – providing the one
constant in the overall research direction and approach to the problem domain.
Dr. Barnat’s research has been focused on a key current problem in the application of logic model
checking techniques: the problem of scaling the search to multiple computers and/or multiple cores on
a single computer. By scaling the search it can become possible to either tackle larger problem sizes, or
to tackle the same problems as before in significantly reduced time. Barnat is one of only a fairly small
number of researchers in this domain who can be credited with a consistent pattern of improvements,
which is reflected in his contributions to one of the leading research systems for distributed model
checking: the DiVine suite of tools. Many of Dr. Barnat’s papers focus on the central problems in this
domain, with in almost all cases theoretical insights carefully verified by empirical evidence. He and his
colleagues have developed and investigated the properties of a range of interesting new algorithms and
data structures, especially for the verification of liveness properties – a class that is traditionally the
most complex to handle efficiently. Each algorithm is explained clearly, and its relatively performance
documented carefully – in the process setting an example to other researchers. The DiVine group, with
Dr. Barnat as a main driving force, is currently one of the most productive research groups in this
domain.
As a peer researcher I can argue with Dr. Barnat on some of the details of the work performed or of
metrics collection, but none of this takes away from my overall impression of the quality of this work,
and the research directions taken, which can only be positive.
I consider Dr. Barnat to be a leading researcher in the area of software verification and distributed logic
model checking techniques, and greatly value his consistent contributions to this field over the last
decade. I therefore consider Dr. Barnat to have more than proven his qualifications for habilitation. In
my professional opinion Dr. Jiří Barnat is richly deserving of this distinction.
Conclusion
In my opinion, Dr. Jiří Barnat’s habilitation thesis of “Platform-Dependent Verification” meets the
standard requirements for a habilitation thesis in the field of Informatics.
Dr. Gerard J. Holzmann
Arcadia, January 30, 2011