Publications
2020
Vladimír Štill:
Analysis of Parallel C++
Programs,
Ph.D. Thesis, 2020. [PDF] [BIB] [URL] [paper page]
Vladimír Štill:
Automatic Test Generation for Haskell
Programming Assignments,
Proceedings of the 2020 ACM Conference on
Innovation and Technology in Computer Science Education (ITiCSE ’20),
June 15–19, 2020, Trondheim, Norway, 2020. [PDF] [BIB] [URL] [paper
page]
2019
Henrich Lauko, Vladimír Štill, Petr Ročkai, Jiří Barnat:
Extending DIVINE with Symbolic Verification
Using SMT,
Tools and Algorithms for the Construction and
Analysis of Systems, 2019. [BIB] [URL]
Vladimír Štill, Jiří Barnat:
Local Nontermination Detection for Parallel
C++ Programs,
Software engineering and formal methods, 2019. [PDF] [BIB] [URL] [paper page]
2018
Petr Ročkai, Vladimír Štill, Ivana Černá, Jiří Barnat:
DiVM: Model checking with LLVM and graph
memory,
Journal of Systems and Software, 2018. [BIB] [URL] [paper page]
Vladimír Štill:
Memory-Model-Aware Analysis of Parallel
Programs,
Advanced Master’s thesis, PhD Thesis Proposal, 2018. [PDF] [BIB] [URL]
Vladimír Štill, Jiří Barnat:
Model Checking of C++ Programs Under the
x86-TSO Memory Model,
Formal Methods and Software
Engineering, 2018. [PDF] [BIB] [URL] [paper page]
2017
Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera,
Henrich Lauko, Jan Mrázek, Petr Ročkai, Vladimír Štill:
Model Checking of C and C++ with DIVINE
4,
Automated Technology for Verification and
Analysis, 2017. [PDF] [BIB] [URL] [paper page]
Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, Jiří
Barnat:
Optimizing and Caching SMT Queries in
SymDIVINE,
Tools and algorithms for the construction and analysis of
systems, 2017. [BIB]
[URL]
Vladimír Štill, Petr Ročkai, Jiří Barnat:
Using Off-the-Shelf Exception Support
Components in C++ Verification,
IEEE International Conference on Software
Quality, Reliability and Security (QRS), 2017. [PDF] [BIB] [URL] [paper page]
2016
Vladimír Štill, Petr Ročkai, Jiří Barnat:
DIVINE: Explicit-State LTL Model Checker,
Tools and Algorithms for the Construction and
Analysis of Systems, 2016. [BIB] [URL]
Vladimír Štill:
LLVM Transformations for Model
Checking,
Master’s thesis, 2016. [PDF] [BIB] [URL]
Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, Kristína
Zákopčanová:
On Verifying C++ Programs with
Probabilities,
ACM Symposium on Applied Computing,
2016. [BIB] [URL]
Vladimír Štill, Petr Ročkai, Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM
Transformations,
Mathematical and Engineering Methods in
Computer Science, Revised Selected Papers, 2016. [BIB] [URL]
2015
Jiří Barnat, Petr Ročkai, Vladimír Štill, Jiří Weiser:
Fast, Dynamically-Sized Concurrent Hash Table,
Model Checking Software (SPIN 2015), 2015. [BIB] [URL]
Petr Ročkai, Vladimír Štill, Jiří Barnat:
Techniques for Memory-Efficient Model
Checking of C and C++ Code,
Software Engineering and Formal
Methods, 2015. [BIB] [URL]
2014
Vladimír Štill, Petr Ročkai, Jiří Barnat:
Context-Switch-Directed Verification in
DIVINE,
Mathematical and Engineering Methods in
Computer Science, 2014. [BIB] [URL]
2013
Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho,
Milan Lenčo, Petr Ročkai, Vladimír Štill, Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model
Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, 2013. [BIB] [URL]
Vladimír Štill:
State space compression for the DiVinE
model checker,
Bachelor’s thesis, 2013. [PDF] [BIB] [URL]