Petr Ročkai

2017

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill:
Model Checking of C and C++ with DIVINE 4,
International Symposium on Automated Technology for Verification and Analysis (ATVA) (to appear), 2017. [bibtex, paper page]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification,
Software Quality, Reliability & Security (to appear), 2017. [bibtex, paper page]

2016

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
DIVINE: Explicit-State LTL Model Checker,
Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2016, 920–922. [bibtex, pdf, url]

Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, and Kristína Zákopčanová:
On Verifying C++ Programs with Probabilities,
ACM Symposium on Applied Computing, 2016, 1238–1243. [bibtex, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations,
Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture Notes in Computer Science, 144–155. [bibtex, pdf, url]

2015

Jiří Barnat, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
Fast, Dynamically-Sized Concurrent Hash Table,
Model Checking Software (SPIN 2015), Springer International Publishing, 2015, volume 9232 of Lecture Notes in Computer Science, 49-65. [bibtex, pdf, url]

Petr Ročkai:
Model Checking Software,
Ph.D. Thesis, 2015. [bibtex, pdf, url]

Petr Ročkai, Vladimír Štill, and Jiří Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code,
Software Engineering and Formal Methods, Springer International Publishing, 2015, volume 9276 of Lecture Notes in Computer Science, 268–282. [bibtex, pdf, url]

2014

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Context-Switch-Directed Verification in DIVINE,
Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146. [bibtex, pdf, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Model Checking C++ with Exceptions,
Automated Verification of Critical Systems, 2014. [bibtex, url]

2013

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868. [bibtex, url]

Jiří Barnat, Jan Havlíček, and Petr Ročkai:
Distributed LTL Model Checking with Hash Compaction,
Electronic Notes in Theoretical Computer Science, Volume 296, Elsevier Science, 2013, 79-93. [bibtex, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Improved State Space Reductions for LTL Model Checking of C & C++ Programs,
NASA Formal Methods (NFM 2013), Springer, 2013, volume 7871 of LNCS, 1–15. [bibtex]

2012

Jiří Barnat, Luboš Brim, and Petr Ročkai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties,
Science of Computer Programming, Elsevier North-Holland, Inc., 2012, 1272–1288. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs,
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 252–266. [bibtex, url]

2010

Jiří Barnat, Luboš Brim, Milan Češka, and Petr Ročkai:
DiVinE: Parallel Distributed Model Checker,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, 2010, 4–7. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Parallel Partial Order Reduction with Topological Sort Proviso,
Proceeding of SEFM 2010, IEEE Computer Society Press, 2010. [bibtex]

Petr Ročkai:
Partial Order Reduction in Parallel Model Checking,
Master’s Thesis, 2010. [bibtex, pdf, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Shared Memory LTL Model Checking,
International Journal on Software Tools for Technology Transfer (STTT), 2010, 139–153. [bibtex, url]

2009

Jiří Barnat, Luboš Brim, and Petr Ročkai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties,
Formal Methods and Software Engineering (ICFEM 2009), Springer, 2009, volume 5885 of LNCS, 407–425. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE 2.0: High-Performance Model Checking,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 31–32. [bibtex]

2008

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE Multi-Core – A Parallel LTL Model-Checker,
Automated Technology for Verification and Analysis (ATVA 2008), Springer, 2008, volume 5311 of LNCS, 234–239. [bibtex]

Petr Ročkai:
Multi-Threaded Nested DFS,
Bachelor’s Thesis, 2008. [bibtex, pdf, url]

Jiří Barnat and Petr Ročkai:
Shared Hash Tables in Parallel Model Checking,
ENTCS, 2008, 79–91. [bibtex]

2007

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Multi-core LTL Model-Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 187–203. [bibtex]

2006

Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai, and Pavel Šimeček:
DiVinE – A Tool for Distributed Verification (Tool Paper),
Computer Aided Verification, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278–281. [bibtex]