Petr Rockai

According to our database, Petr Rockai authored at least 37 papers between 2006 and 2022.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2022

Verification of Programs Sensitive to Heap Layout.

Henrich Lauko, Lukás Korencik, Petr Rockai

ACM Trans. Softw. Eng. Methodol., 2022

DivSIM , an interactive simulator for LLVM bitcode.

Petr Rockai, Jiri Barnat

Int. J. Softw. Tools Technol. Transf., 2022

LART: Compiled Abstract Execution - (Competition Contribution).

Henrich Lauko, Petr Rockai

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

2021

Reproducible execution of POSIX programs with DiOS.

Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat

Softw. Syst. Model., 2021

2020

On Symbolic Execution of Decompiled Programs.

Lukás Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat

Proceedings of the 20th IEEE International Conference on Software Quality, 2020

2019

Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution).

Henrich Lauko, Vladimír Still, Petr Rockai, Jiri Barnat

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

String Abstraction for Model Checking of C Programs.

Agostino Cortesi, Henrich Lauko, Martina Olliaro, Petr Rockai

Proceedings of the Model Checking Software - 26th International Symposium, 2019

A Simulator for LLVM Bitcode.

Petr Rockai, Jiri Barnat

Proceedings of the Formal Methods for Industrial Critical Systems, 2019

Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table.

Petr Rockai

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Compiling C and C++ Programs for Dynamic White-Box Analysis.

Zuzana Baranová, Petr Rockai

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

2018

DiVM: Model checking with LLVM and graph memory.

Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat

J. Syst. Softw., 2018

Symbolic Computation via Program Transformation.

Henrich Lauko, Petr Rockai, Jiri Barnat

Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

2017

DiVM: Model Checking with LLVM and Graph Memory.

Petr Rockai, Ivana Cerná, Jiri Barnat

CoRR, 2017

From Model Checking to Runtime Verification and Back.

Katarína Kejstová, Petr Rockai, Jiri Barnat

Proceedings of the Runtime Verification - 17th International Conference, 2017

Using Off-the-Shelf Exception Support Components in C++ Verification.

Vladimír Still, Petr Rockai, Jiri Barnat

Proceedings of the 2017 IEEE International Conference on Software Quality, 2017

Model Checking of C and C++ with DIVINE 4.

Zuzana Baranová, Jiri Barnat, Katarína Kejstová, Tadeás Kucera, Henrich Lauko, Jan Mrázek, Petr Rockai, Vladimír Still

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Model checking C++ programs with exceptions.

Petr Rockai, Jiri Barnat, Lubos Brim

Sci. Comput. Program., 2016

DIVINE: Explicit-State LTL Model Checker - (Competition Contribution).

Vladimír Still, Petr Rockai, Jiri Barnat

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

On verifying C++ programs with probabilities.

Jiri Barnat, Ivana Cerná, Petr Rockai, Vladimír Still, Kristína Zákopcanová

Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

2015

Fast, Dynamically-Sized Concurrent Hash Table.

Jiri Barnat, Petr Rockai, Vladimír Still, Jirí Weiser

Proceedings of the Model Checking Software - 22nd International Symposium, 2015

Techniques for Memory-Efficient Model Checking of C and C++ Code.

Petr Rockai, Vladimír Still, Jiri Barnat

Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

Weak Memory Models as LLVM-to-LLVM Transformations.

Vladimír Still, Petr Rockai, Jiri Barnat

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2015

2014

Model Checking C++ with Exceptions.

Petr Rockai, Jiri Barnat, Lubos Brim

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

Context-Switch-Directed Verification in DIVINE.

Vladimír Still, Petr Rockai, Jiri Barnat

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2014

2013

Improved State Space Reductions for LTL Model Checking of C and C++ Programs.

Petr Rockai, Jiri Barnat, Lubos Brim

Proceedings of the NASA Formal Methods, 2013

DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs.

Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, Jirí Weiser

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties.

Jiri Barnat, Lubos Brim, Petr Rockai

Sci. Comput. Program., 2012

Distributed LTL Model Checking with Hash Compaction.

Jiri Barnat, Jan Havlícek, Petr Rockai

Proceedings of the Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling, 2012

Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs.

Jiri Barnat, Lubos Brim, Petr Rockai

Proceedings of the NASA Formal Methods, 2012

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs.

Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai

Proceedings of the Formal Methods for Industrial Critical Systems, 2012

2010

Scalable shared memory LTL model checking.

Jiri Barnat, Lubos Brim, Petr Rockai

Int. J. Softw. Tools Technol. Transf., 2010

Parallel Partial Order Reduction with Topological Sort Proviso.

Jiri Barnat, Lubos Brim, Petr Rockai

Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

2009

A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.

Jiri Barnat, Lubos Brim, Petr Rockai

Proceedings of the Formal Methods and Software Engineering, 2009

2008

DiVinE Multi-Core - A Parallel LTL Model-Checker.

Jiri Barnat, Lubos Brim, Petr Rockai

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Shared Hash Tables in Parallel Model Checking.

Jiri Barnat, Petr Rockai

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Scalable Multi-core LTL Model-Checking.

Jiri Barnat, Lubos Brim, Petr Rockai

Proceedings of the Model Checking Software, 2007

2006

DiVinE - A Tool for Distributed Verification.

Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek

Proceedings of the Computer Aided Verification, 18th International Conference, 2006