Jiri Barnat

120 papers A* 6A 7B 14C 16Misc 2Journal 34Unranked 39
YearRankTypeTitle / Venue / Authors
2024 A conf
Tree-Based Reconfiguration of Metamorphic Robots.
IROS
Patrick Ondika, Jan Mrázek, Jiri Barnat
2023 — conf
Fault-Tolerant and System-Wide Communication for Metamorphic Robots.
CASE
Jan Mrázek, Vladimír Chlup, Jiri Barnat
2023 — conf
RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots.
CASE
Jan Mrázek, Jiri Barnat
2023 A* conf
Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics.
ICRA
Jan Mrázek, Patrick Ondika, Ivana Cerná, Jiri Barnat
2022 J jnl
DivSIM , an interactive simulator for LLVM bitcode.
Int. J. Softw. Tools Technol. Transf.
Petr Rockai, Jiri Barnat
2021 A conf
Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way?
IROS
Jan Mrázek, Martin Jonás, Jiri Barnat
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
Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution).
TACAS (3)
Henrich Lauko, Vladimír Still, Petr Rockai, Jiri Barnat
2019 B conf
Local Nontermination Detection for Parallel C++ Programs.
SEFM
Vladimír Still, Jiri Barnat
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 A conf
RoFICoM - First Open-Hardware Connector for Metamorphic Robots.
IROS
Jan Mrázek, Jiri Barnat
2018 J jnl
DiVM: Model checking with LLVM and graph memory.
J. Syst. Softw.
Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat
2018 C ed.
Formal Methods for Industrial Critical Systems - 23rd International Conference, FMICS 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings
FMICS
Falk Howar, Jiri Barnat
2018 J jnl
From Model Checking to Runtime Verification and Back.
CoRR
Katarína Kejstová, Petr Rockai, Jiri Barnat
2018 C conf
Model Checking of C++ Programs Under the x86-TSO Memory Model.
ICFEM
Vladimír Still, Jiri Barnat
2018 J jnl
On clock-aware LTL parameter synthesis of timed automata.
J. Log. Algebraic Methods Program.
Peter Bezdek, Nikola Benes, Ivana Cerná, Jiri Barnat
2018 — ch.
Parallel Model Checking Algorithms for Linear-Time Temporal Logic.
Handbook of Parallel Constraint Reasoning
Jiri Barnat, Vincent Bloemen, Alexandre Duret-Lutz, Alfons Laarman, Laure Petrucci, Jaco van de Pol, Etienne Renault
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 — conf
Detecting Attractors in Biological Models with Uncertain Parameters.
CMSB
Jiri Barnat, Nikola Benes, Lubos Brim, Martin Demko, Matej Hajnal, Samuel Pastva, David Safránek
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 — conf
Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution).
TACAS (2)
Jan Mrázek, Martin Jonás, Vladimír Still, Henrich Lauko, Jiri Barnat
2017 J jnl
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking.
CoRR
Jan Mrázek, Martin Jonás, Jiri Barnat
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 J jnl
Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories.
Softw. Qual. J.
Petr Bauch, Vojtech Havel, Jiri Barnat
2016 J jnl
Analysing sanity of requirements for avionics systems.
Formal Aspects Comput.
Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila
2016 J jnl
Control Explicit-Data Symbolic Model Checking.
ACM Trans. Softw. Eng. Methodol.
Petr Bauch, Vojtech Havel, Jiri Barnat
2016 A conf
DIVINE: Explicit-State LTL Model Checker - (Competition Contribution).
TACAS
Vladimír Still, Petr Rockai, Jiri Barnat
2016 B conf
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis.
SEFM
Jaroslav Bendík, Nikola Benes, Jiri Barnat, Ivana Cerná
2016 B conf
LTL Parameter Synthesis of Parametric Timed Automata.
SEFM
Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná
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á
2016 J jnl
Optimal Observation Mode Scheduling for Systems under Temporal Constraints.
CoRR
Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerná
2016 C conf
Optimal observation mode scheduling for systems under temporal constraints.
ACC
Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerna
2016 — conf
Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components.
Euro-Par Workshops
Stefano Aldegheri, Jiri Barnat, Nicola Bombieri, Federico Busato, Milan Ceska
2016 — conf
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration.
SPIN
Jan Mrázek, Petr Bauch, Henrich Lauko, Jiri Barnat
2016 — conf
Tunable Online MUS/MSS Enumeration.
FSTTCS
Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat
2016 J jnl
Tunable Online MUS/MSS Enumeration.
CoRR
Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat
2015 J jnl
Analysing Sanity of Requirements for Avionics Systems (Preliminary Version).
CoRR
Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila
2015 — conf
Fast, Dynamically-Sized Concurrent Hash Table.
SPIN
Jiri Barnat, Petr Rockai, Vladimír Still, Jirí Weiser
2015 B conf
Quo Vadis Explicit-State Model Checking.
SOFSEM
Jiri Barnat
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 — conf
LTL Model Checking of LLVM Bitcode with Symbolic Data.
MEMICS
Petr Bauch, Vojtech Havel, Jiri Barnat
2014 J jnl
LTL Model Checking of Parametric Timed Automata.
CoRR
Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná
2014 J jnl
Model Checking C++ with Exceptions.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Petr Rockai, Jiri Barnat, Lubos Brim
2014 C conf
Model Checking Parallel Programs with Inputs.
PDP
Jiri Barnat, Petr Bauch, Vojtech Havel
2014 C conf
On Clock-Aware LTL Properties of Timed Automata.
ICTAC
Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná
2014 — conf
Temporal Verification of Simulink Diagrams.
HASE
Jiri Barnat, Petr Bauch, Vojtech Havel
2013 J jnl
Control Explicit---Data Symbolic Model Checking: An Introduction
CoRR
Jiri Barnat, Petr Bauch
2013 — conf
DCCL: verification of component systems with ensembles.
CBSE
Jiri Barnat, Nikola Benes, Ivana Cerná, Zuzana Petruchová
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 J jnl
Formal analysis of piecewise affine systems through formula-guided refinement.
Autom.
Boyan Yordanov, Jana Tumova, Ivana Cerná, Jiri Barnat, Calin Belta
2013 — conf
Improved State Space Reductions for LTL Model Checking of C and C++ Programs.
NASA Formal Methods
Petr Rockai, Jiri Barnat, Lubos Brim
2013 — conf
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model.
ACSD
Jiri Barnat, Lubos Brim, Vojtech Havel
2013 — conf
Towards Verification of Ensemble-Based Component Systems.
FACS
Jiri Barnat, Nikola Benes, Tomás Bures, Ivana Cerná, Jaroslav Keznikl, Frantisek Plásil
2012 J jnl
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints
CoRR
María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna
2012 — conf
Attraction-based receding horizon path planning with temporal logic constraints.
CDC
María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna
2012 B conf
Checking Sanity of Software Requirements.
SEFM
Jiri Barnat, Petr Bauch, Lubos Brim
2012 J jnl
Designing fast LTL model checking algorithms for many-core GPUs.
J. Parallel Distributed Comput.
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
2012 — conf
Distributed LTL Model Checking with Hash Compaction.
PASM/PDMC
Jiri Barnat, Jan Havlícek, Petr Rockai
2012 Misc conf
Executing Model Checking Counterexamples in Simulink.
TASE
Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira
2012 J jnl
On Parameter Synthesis by Parallel Model Checking.
IEEE ACM Trans. Comput. Biol. Bioinform.
Jiri Barnat, Lubos Brim, Adam Krejci, Adam Streck, David Safránek, Martin Vejnar, Tomas Vejpustek
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 J jnl
Temporal Logic Control of Discrete-Time Piecewise Affine Systems.
IEEE Trans. Autom. Control.
Boyan Yordanov, Jana Tumova, Ivana Cerna, Jiri Barnat, Calin Belta
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
2012 J jnl
Verification of Systems with Degradation.
Comput. Informatics
Jiri Barnat, Ivana Cerná, Jana Tumova
2011 — conf
Computing Optimal Cycle Mean in Parallel on CUDA
PDMC
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
2011 A conf
Computing Strongly Connected Components in Parallel on CUDA.
IPDPS
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
2011 J jnl
Distributed Algorithms for SCC Decomposition.
J. Log. Comput.
Jiri Barnat, Jakub Chaloupka, Jaco van de Pol
2011 J jnl
Flash memory efficient LTL model checking.
Sci. Comput. Program.
Stefan Edelkamp, Damian Sulewski, Jiri Barnat, Lubos Brim, Pavel Simecek
2011 — conf
Platform Dependent Verification: On Engineering Verification Tools for 21st Century
PDMC
Lubos Brim, Jiri Barnat
2011 — ed.
Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snowbird, Utah, USA, July 14, 2011.
PDMC
Jiri Barnat, Keijo Heljanko
2011 — conf
Timed Automata Approach to Verification of Systems with Degradation.
MEMICS
Jiri Barnat, Ivana Cerná, Jana Tumova
2010 — conf
A symbolic approach to controlling piecewise affine systems.
CDC
Jana Tumova, Boyan Yordanov, Calin Belta, Ivana Cerna, Jiri Barnat
2010 B conf
Employing Multiple CUDA Devices to Accelerate LTL Model Checking.
ICPADS
Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska
2010 — conf
Formal analysis of piecewise affine systems through formula-guided refinement.
CDC
Boyan Yordanov, Jana Tumova, Calin Belta, Ivana Cerna, Jiri Barnat
2010 J jnl
High-performance analysis of biological systems dynamics with the DiVinE model checker.
Briefings Bioinform.
Jiri Barnat, Lubos Brim, David Safránek
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
2009 — conf
BioDiVinE: A Framework for Parallel Analysis of Biological Models
COMPMOD
Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, Jana Fabriková, Jan Láník, David Safránek, Hongwu Ma
2009 B conf
CUDA Accelerated LTL Model Checking.
ICPADS
Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr
2009 A* conf
Cluster-Based I/O-Efficient LTL Model Checking.
ASE
Jiri Barnat, Lubos Brim, Pavel Simecek
2009 — conf
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking
PDMC
Jiri Barnat, Lubos Brim, Milan Ceska
2009 A conf
Efficient large-scale model checking.
IPDPS
Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim
2009 J jnl
On algorithmic analysis of transcriptional regulation by LTL model checking.
Theor. Comput. Sci.
Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, Jana Fabriková, David Safránek
2009 — conf
Quantitative Model Checking of Systems with Degradation.
QEST
Jiri Barnat, Ivana Cerná, Jana Tumova
2008 C conf
Can Flash Memory Help in Model Checking?
FMICS
Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek
2008 B conf
DiVinE Multi-Core - A Parallel LTL Model-Checker.
ATVA
Jiri Barnat, Lubos Brim, Petr Rockai
2008 — conf
Efficient Large-Scale Model Checking.
Distributed Verification and Grid Computing
Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim
2008 C conf
Local Quantitative LTL Model Checking.
FMICS
Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova
2008 — conf
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems.
QEST
Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova
2008 A conf
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking.
TACAS
Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber
2008 C conf
Squeeze All the Power Out of Your Hardware to Verify Your Software!.
ISoLA
Jiri Barnat, Lubos Brim
2007 A* conf
I/O Efficient Accepting Cycle Detection.
CAV
Jiri Barnat, Lubos Brim, Pavel Simecek
2007 — conf
Improved Distributed Algorithms for SCC Decomposition.
PDMC@CAV
Jiri Barnat, Jakub Chaloupka, Jaco van de Pol
2007 — conf
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE.
FBTC@CONCUR
Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, David Safránek
2007 B conf
Parallel Model Checking and the FMICS-jETI Platform.
ICECCS
Jiri Barnat, Lubos Brim, Martin Leucker
2007 — conf
ProbDiVinE: A Parallel Qualitative LTL Model Checker.
QEST
Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova
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
2007 — conf
Tutorial: Parallel Model Checking.
SPIN
Lubos Brim, Jiri Barnat
2006 A* conf
DiVinE - A Tool for Distributed Verification.
CAV
Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek
2006 J jnl
Distributed breadth-first search LTL model checking.
Formal Methods Syst. Des.
Jiri Barnat, Ivana Cerná
2006 — conf
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs.
FMICS/PDMC
Jiri Barnat, Pavel Moravec
2005 — conf
Cluster-Based LTL Model Checking of Large Systems.
FMCO
Jiri Barnat, Lubos Brim, Ivana Cerná
2004 C conf
From Distributed Memory Cycle Detection to Parallel LTL Model Checking.
FMICS
Jiri Barnat, Lubos Brim, Jakub Chaloupka
2003 C conf
Distribution of Explicit-State LTL Model-Checking.
FMICS
Lubos Brim, Jiri Barnat
2003 A* conf
Parallel Breadth-First Search LTL Model-Checking.
ASE
Jiri Barnat, Lubos Brim, Jakub Chaloupka
2001 — conf
Distributed LTL Model-Checking in SPIN.
SPIN
Jiri Barnat, Lubos Brim, Jitka Stríbrná