Petr Rockai

Publication Activity (10 Years)

Years Active: 2006-2022
Publications (10 Years): 25

Top Topics

Temporal Properties

Automated Verification

Top Venues

FM Workshops (1)

Publications

Henrich Lauko, Lukás Korencik, Petr Rockai
Verification of Programs Sensitive to Heap Layout. ACM Trans. Softw. Eng. Methodol. 31 (4) (2022)
Petr Rockai, Jiri Barnat
DivSIM , an interactive simulator for LLVM bitcode. Int. J. Softw. Tools Technol. Transf. 24 (3) (2022)
Henrich Lauko, Petr Rockai
LART: Compiled Abstract Execution - (Competition Contribution). TACAS (2) (2022)
Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat
Reproducible execution of POSIX programs with DiOS. Softw. Syst. Model. 20 (2) (2021)
Lukás Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat
On Symbolic Execution of Decompiled Programs. QRS (2020)
Petr Rockai
Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table. FM Workshops (1) (2019)
Petr Rockai, Jiri Barnat
A Simulator for LLVM Bitcode. FMICS (2019)
Zuzana Baranová, Petr Rockai
Compiling C and C++ Programs for Dynamic White-Box Analysis. FM Workshops (1) (2019)
Henrich Lauko, Vladimír Still, Petr Rockai, Jiri Barnat
Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). TACAS (3) (2019)
Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat
Reproducible Execution of POSIX Programs with DiOS. CoRR (2019)
Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat
Reproducible Execution of POSIX Programs with DiOS. SEFM (2019)
Agostino Cortesi, Henrich Lauko, Martina Olliaro, Petr Rockai
String Abstraction for Model Checking of C Programs. SPIN (2019)
Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat
DiVM: Model checking with LLVM and graph memory. J. Syst. Softw. 143 (2018)
Katarína Kejstová, Petr Rockai, Jiri Barnat
From Model Checking to Runtime Verification and Back. CoRR (2018)
Henrich Lauko, Petr Rockai, Jiri Barnat
Symbolic Computation via Program Transformation. ICTAC (2018)
Henrich Lauko, Petr Rockai, Jiri Barnat
Symbolic Computation via Program Transformation. CoRR (2018)
Vladimír Still, Petr Rockai, Jiri Barnat
Using Off-the-Shelf Exception Support Components in C++ Verification. QRS (2017)
Petr Rockai, Ivana Cerná, Jiri Barnat
DiVM: Model Checking with LLVM and Graph Memory. CoRR (2017)
Zuzana Baranová, Jiri Barnat, Katarína Kejstová, Tadeás Kucera, Henrich Lauko, Jan Mrázek, Petr Rockai, Vladimír Still
Model Checking of C and C++ with DIVINE 4. ATVA (2017)
Katarína Kejstová, Petr Rockai, Jiri Barnat
From Model Checking to Runtime Verification and Back. RV (2017)
Vladimír Still, Petr Rockai, Jiri Barnat
Using Off-the-Shelf Exception Support Components in C++ Verification. CoRR (2017)
Petr Rockai, Jiri Barnat
A Simulator for LLVM Bitcode. CoRR (2017)
Vladimír Still, Petr Rockai, Jiri Barnat
DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). TACAS (2016)
Jiri Barnat, Ivana Cerná, Petr Rockai, Vladimír Still, Kristína Zákopcanová
On verifying C++ programs with probabilities. SAC (2016)
Petr Rockai, Jiri Barnat, Lubos Brim
Model checking C++ programs with exceptions. Sci. Comput. Program. 128 (2016)
Vladimír Still, Petr Rockai, Jiri Barnat
Weak Memory Models as LLVM-to-LLVM Transformations. MEMICS (2015)
Jiri Barnat, Petr Rockai, Vladimír Still, Jirí Weiser
Fast, Dynamically-Sized Concurrent Hash Table. SPIN (2015)
Petr Rockai, Vladimír Still, Jiri Barnat
Techniques for Memory-Efficient Model Checking of C and C++ Code. SEFM (2015)
Petr Rockai, Jiri Barnat, Lubos Brim
Model Checking C++ with Exceptions. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014)
Vladimír Still, Petr Rockai, Jiri Barnat
Context-Switch-Directed Verification in DIVINE. MEMICS (2014)
Petr Rockai, Jiri Barnat, Lubos Brim
Improved State Space Reductions for LTL Model Checking of C and C++ Programs. NASA Formal Methods (2013)
Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, Jirí Weiser
DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. CAV (2013)
Jiri Barnat, Jan Havlícek, Petr Rockai
Distributed LTL Model Checking with Hash Compaction. Electron. Notes Theor. Comput. Sci. 296 (2013)
Jiri Barnat, Lubos Brim, Petr Rockai
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NASA Formal Methods (2012)
Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. FMICS (2012)
Jiri Barnat, Lubos Brim, Petr Rockai
On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77 (12) (2012)
Jiri Barnat, Lubos Brim, Petr Rockai
Parallel Partial Order Reduction with Topological Sort Proviso. SEFM (2010)
Jiri Barnat, Lubos Brim, Petr Rockai
Scalable shared memory LTL model checking. Int. J. Softw. Tools Technol. Transf. 12 (2) (2010)
Jiri Barnat, Lubos Brim, Petr Rockai
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. ICFEM (2009)
Jiri Barnat, Lubos Brim, Petr Rockai
DiVinE Multi-Core - A Parallel LTL Model-Checker. ATVA (2008)
Jiri Barnat, Petr Rockai
Shared Hash Tables in Parallel Model Checking. Electron. Notes Theor. Comput. Sci. 198 (1) (2008)
Jiri Barnat, Lubos Brim, Petr Rockai
Scalable Multi-core LTL Model-Checking. SPIN (2007)
Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek
DiVinE - A Tool for Distributed Verification. CAV (2006)