Publications

2020

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. [BIB] [PDF] [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. [BIB] [PDF] [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. [BIB] [PDF] [URL]

Vladimír Štill, Jiří Barnat:
Model Checking of C++ Programs Under the x86-TSO Memory Model,
Formal Methods and Software Engineering, 2018. [BIB] [PDF] [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. [BIB] [PDF] [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. [BIB] [PDF] [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. [BIB] [PDF] [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. [BIB] [PDF] [URL]