Petr Rockai

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