Jiri Barnat

Publication Activity (10 Years)

Years Active: 2001-2023
Publications (10 Years): 47

Top Venues

CoRR

SEFM

MEMICS

ICTAC

Publications

Jan Mrázek, Vladimír Chlup, Jiri Barnat
Fault-Tolerant and System-Wide Communication for Metamorphic Robots. CASE (2023)
Jan Mrázek, Jiri Barnat
RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots. CASE (2023)
Jan Mrázek, Patrick Ondika, Ivana Cerná, Jiri Barnat
Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics. ICRA (2023)
Petr Rockai, Jiri Barnat
DivSIM , an interactive simulator for LLVM bitcode. Int. J. Softw. Tools Technol. Transf. 24 (3) (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)
Jan Mrázek, Martin Jonás, Jiri Barnat
Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? IROS (2021)
Lukás Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat
On Symbolic Execution of Decompiled Programs. QRS (2020)
Petr Rockai, Jiri Barnat
A Simulator for LLVM Bitcode. FMICS (2019)
Vladimír Still, Jiri Barnat
Local Nontermination Detection for Parallel C++ Programs. SEFM (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)
Jan Mrázek, Jiri Barnat
RoFICoM - First Open-Hardware Connector for Metamorphic Robots. IROS (2019)
Peter Bezdek, Nikola Benes, Ivana Cerná, Jiri Barnat
On clock-aware LTL parameter synthesis of timed automata. J. Log. Algebraic Methods Program. 99 (2018)
Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat
DiVM: Model checking with LLVM and graph memory. J. Syst. Softw. 143 (2018)
Vladimír Still, Jiri Barnat
Model Checking of C++ Programs Under the x86-TSO Memory Model. ICFEM (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)
Jan Mrázek, Martin Jonás, Vladimír Still, Henrich Lauko, Jiri Barnat
Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). TACAS (2) (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)
Jiri Barnat, Nikola Benes, Lubos Brim, Martin Demko, Matej Hajnal, Samuel Pastva, David Safránek
Detecting Attractors in Biological Models with Uncertain Parameters. CMSB (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)
Jan Mrázek, Martin Jonás, Jiri Barnat
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking. CoRR (2017)
Petr Bauch, Vojtech Havel, Jiri Barnat
Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. Softw. Qual. J. 24 (1) (2016)
Vladimír Still, Petr Rockai, Jiri Barnat
DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). TACAS (2016)
Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerná
Optimal Observation Mode Scheduling for Systems under Temporal Constraints. CoRR (2016)
Jan Mrázek, Petr Bauch, Henrich Lauko, Jiri Barnat
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. SPIN (2016)
Jaroslav Bendík, Nikola Benes, Jiri Barnat, Ivana Cerná
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. SEFM (2016)
Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila
Analysing sanity of requirements for avionics systems. Formal Aspects Comput. 28 (1) (2016)
Petr Bauch, Vojtech Havel, Jiri Barnat
Control Explicit-Data Symbolic Model Checking. ACM Trans. Softw. Eng. Methodol. 25 (2) (2016)
Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat
Tunable Online MUS/MSS Enumeration. FSTTCS (2016)
Stefano Aldegheri, Jiri Barnat, Nicola Bombieri, Federico Busato, Milan Ceska
Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. Euro-Par Workshops (2016)
Jiri Barnat, Ivana Cerná, Petr Rockai, Vladimír Still, Kristína Zákopcanová
On verifying C++ programs with probabilities. SAC (2016)
Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná
LTL Parameter Synthesis of Parametric Timed Automata. SEFM (2016)
Petr Rockai, Jiri Barnat, Lubos Brim
Model checking C++ programs with exceptions. Sci. Comput. Program. 128 (2016)
Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerna
Optimal observation mode scheduling for systems under temporal constraints. ACC (2016)
Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat
Tunable Online MUS/MSS Enumeration. CoRR (2016)
Vladimír Still, Petr Rockai, Jiri Barnat
Weak Memory Models as LLVM-to-LLVM Transformations. MEMICS (2015)
Jiri Barnat
Quo Vadis Explicit-State Model Checking. SOFSEM (2015)
Jiri Barnat, Petr Rockai, Vladimír Still, Jirí Weiser
Fast, Dynamically-Sized Concurrent Hash Table. SPIN (2015)
Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila
Analysing Sanity of Requirements for Avionics Systems (Preliminary Version). CoRR (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)
Jiri Barnat, Petr Bauch, Vojtech Havel
Temporal Verification of Simulink Diagrams. HASE (2014)
Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná
On Clock-Aware LTL Properties of Timed Automata. ICTAC (2014)
Vladimír Still, Petr Rockai, Jiri Barnat
Context-Switch-Directed Verification in DIVINE. MEMICS (2014)
Petr Bauch, Vojtech Havel, Jiri Barnat
LTL Model Checking of LLVM Bitcode with Symbolic Data. MEMICS (2014)
Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná
LTL Model Checking of Parametric Timed Automata. CoRR (2014)
Jiri Barnat, Petr Bauch, Vojtech Havel
Model Checking Parallel Programs with Inputs. PDP (2014)
Jiri Barnat, Petr Bauch
Control Explicit---Data Symbolic Model Checking: An Introduction CoRR (2013)
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, Nikola Benes, Tomás Bures, Ivana Cerná, Jaroslav Keznikl, Frantisek Plasil
Towards Verification of Ensemble-Based Component Systems. FACS (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, Nikola Benes, Ivana Cerná, Zuzana Petruchová
DCCL: verification of component systems with ensembles. CBSE (2013)
Boyan Yordanov, Jana Tumova, Ivana Cerná, Jiri Barnat, Calin Belta
Formal analysis of piecewise affine systems through formula-guided refinement. Autom. 49 (1) (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, Vojtech Havel
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD (2013)
Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira
Executing Model Checking Counterexamples in Simulink. TASE (2012)
Jiri Barnat, Lubos Brim, Petr Rockai
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NASA Formal Methods (2012)
Jiri Barnat, Petr Bauch, Lubos Brim
Checking Sanity of Software Requirements. SEFM (2012)
Boyan Yordanov, Jana Tumova, Ivana Cerna, Jiri Barnat, Calin Belta
Temporal Logic Control of Discrete-Time Piecewise Affine Systems. IEEE Trans. Autom. Control. 57 (6) (2012)
María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints CoRR (2012)
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distributed Comput. 72 (9) (2012)
Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. FMICS (2012)
María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna
Attraction-based receding horizon path planning with temporal logic constraints. CDC (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, Adam Krejci, Adam Streck, David Safránek, Martin Vejnar, Tomas Vejpustek
On Parameter Synthesis by Parallel Model Checking. IEEE ACM Trans. Comput. Biol. Bioinform. 9 (3) (2012)
Jiri Barnat, Ivana Cerná, Jana Tumova
Verification of Systems with Degradation. Comput. Informatics 31 (3) (2012)
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
Computing Strongly Connected Components in Parallel on CUDA. IPDPS (2011)
Jiri Barnat, Jakub Chaloupka, Jaco van de Pol
Distributed Algorithms for SCC Decomposition. J. Log. Comput. 21 (1) (2011)
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
Computing Optimal Cycle Mean in Parallel on CUDA PDMC (2011)
Jiri Barnat, Ivana Cerná, Jana Tumova
Timed Automata Approach to Verification of Systems with Degradation. MEMICS (2011)
Lubos Brim, Jiri Barnat
Platform Dependent Verification: On Engineering Verification Tools for 21st Century PDMC (2011)
Stefan Edelkamp, Damian Sulewski, Jiri Barnat, Lubos Brim, Pavel Simecek
Flash memory efficient LTL model checking. Sci. Comput. Program. 76 (2) (2011)
Boyan Yordanov, Jana Tumova, Calin Belta, Ivana Cerna, Jiri Barnat
Formal analysis of piecewise affine systems through formula-guided refinement. CDC (2010)
Jana Tumova, Boyan Yordanov, Calin Belta, Ivana Cerna, Jiri Barnat
A symbolic approach to controlling piecewise affine systems. CDC (2010)
Jiri Barnat, Lubos Brim, David Safránek
High-performance analysis of biological systems dynamics with the DiVinE model checker. Briefings Bioinform. 11 (3) (2010)
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS (2010)
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, Ivana Cerná, Sven Drazan, Jana Fabriková, David Safránek
On algorithmic analysis of transcriptional regulation by LTL model checking. Theor. Comput. Sci. 410 (33-34) (2009)
Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr
CUDA Accelerated LTL Model Checking. ICPADS (2009)
Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, Jana Fabriková, Jan Láník, David Safránek, Hongwu Ma
BioDiVinE: A Framework for Parallel Analysis of Biological Models COMPMOD (2009)
Jiri Barnat, Lubos Brim, Pavel Simecek
Cluster-Based I/O-Efficient LTL Model Checking. ASE (2009)
Jiri Barnat, Lubos Brim, Milan Ceska
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking PDMC (2009)
Jiri Barnat, Ivana Cerná, Jana Tumova
Quantitative Model Checking of Systems with Degradation. QEST (2009)
Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim
Efficient large-scale model checking. IPDPS (2009)
Jiri Barnat, Lubos Brim, Petr Rockai
DiVinE Multi-Core - A Parallel LTL Model-Checker. ATVA (2008)
Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. TACAS (2008)
Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek
Can Flash Memory Help in Model Checking? FMICS (2008)
Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, David Safránek
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. Electron. Notes Theor. Comput. Sci. 194 (3) (2008)
Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim
Efficient Large-Scale Model Checking. Distributed Verification and Grid Computing (2008)
Jiri Barnat, Jakub Chaloupka, Jaco van de Pol
Improved Distributed Algorithms for SCC Decomposition. Electron. Notes Theor. Comput. Sci. 198 (1) (2008)
Jiri Barnat, Lubos Brim
Squeeze All the Power Out of Your Hardware to Verify Your Software!. ISoLA (2008)

Jiri Barnat.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Jiri Barnat