Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJiri Barnat
Person information
- affiliation: Masaryk University, Brno, Czech Republic
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[c81]Jan Mrázek, Jiri Barnat:
RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots. CASE 2023: 1-8- [c80]Jan Mrázek, Vladimír Chlup, Jiri Barnat:
Fault-Tolerant and System-Wide Communication for Metamorphic Robots. CASE 2023: 1-8 - [c79]Jan Mrázek, Patrick Ondika, Ivana Cerná, Jiri Barnat:
Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics. ICRA 2023: 11894-11900 - 2022
- [j21]Petr Rockai, Jiri Barnat:
DivSIM , an interactive simulator for LLVM bitcode. Int. J. Softw. Tools Technol. Transf. 24(3): 493-510 (2022) - 2021
- [j20]Petr Rockai
, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat:
Reproducible execution of POSIX programs with DiOS. Softw. Syst. Model. 20(2): 363-382 (2021) - [c78]Jan Mrázek, Martin Jonás, Jiri Barnat:
Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? IROS 2021: 6935-6940 - 2020
- [c77]Lukás Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat:
On Symbolic Execution of Decompiled Programs. QRS 2020: 265-272
2010 – 2019
- 2019
- [c76]Petr Rockai, Jiri Barnat:
A Simulator for LLVM Bitcode. FMICS 2019: 127-142 - [c75]Jan Mrázek, Jiri Barnat:
RoFICoM - First Open-Hardware Connector for Metamorphic Robots. IROS 2019: 2720-2725 - [c74]Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat:
Reproducible Execution of POSIX Programs with DiOS. SEFM 2019: 333-349 - [c73]Vladimír Still, Jiri Barnat:
Local Nontermination Detection for Parallel C++ Programs. SEFM 2019: 373-390 - [c72]Henrich Lauko, Vladimír Still, Petr Rockai, Jiri Barnat:
Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). TACAS (3) 2019: 204-208 - [i14]Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat:
Reproducible Execution of POSIX Programs with DiOS. CoRR abs/1907.03356 (2019) - 2018
- [j19]Peter Bezdek, Nikola Benes, Ivana Cerná, Jiri Barnat:
On clock-aware LTL parameter synthesis of timed automata. J. Log. Algebraic Methods Program. 99: 114-142 (2018) - [j18]Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat:
DiVM: Model checking with LLVM and graph memory. J. Syst. Softw. 143: 1-13 (2018) - [c71]Vladimír Still, Jiri Barnat:
Model Checking of C++ Programs Under the x86-TSO Memory Model. ICFEM 2018: 124-140 - [c70]Henrich Lauko, Petr Rockai, Jiri Barnat:
Symbolic Computation via Program Transformation. ICTAC 2018: 313-332 - [p1]Jiri Barnat, Vincent Bloemen, Alexandre Duret-Lutz, Alfons Laarman, Laure Petrucci, Jaco van de Pol, Etienne Renault:
Parallel Model Checking Algorithms for Linear-Time Temporal Logic. Handbook of Parallel Constraint Reasoning 2018: 457-507 - [e2]Falk Howar, Jiri Barnat:
Formal Methods for Industrial Critical Systems - 23rd International Conference, FMICS 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings. Lecture Notes in Computer Science 11119, Springer 2018, ISBN 978-3-030-00243-5 [contents] - [i13]Katarína Kejstová, Petr Rockai, Jiri Barnat:
From Model Checking to Runtime Verification and Back. CoRR abs/1805.12428 (2018) - [i12]Henrich Lauko, Petr Rockai, Jiri Barnat:
Symbolic Computation via Program Transformation. CoRR abs/1806.03959 (2018) - 2017
- [c69]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: 201-207 - [c68]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: 40-56 - [c67]Vladimír Still, Petr Rockai, Jiri Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification. QRS 2017: 54-64 - [c66]Katarína Kejstová, Petr Rockai, Jiri Barnat:
From Model Checking to Runtime Verification and Back. RV 2017: 225-240 - [c65]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: 390-393 - [i11]Vladimír Still, Petr Rockai, Jiri Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification. CoRR abs/1703.02394 (2017) - [i10]Petr Rockai, Ivana Cerná, Jiri Barnat:
DiVM: Model Checking with LLVM and Graph Memory. CoRR abs/1703.05341 (2017) - [i9]Petr Rockai, Jiri Barnat:
A Simulator for LLVM Bitcode. CoRR abs/1704.05551 (2017) - [i8]Jan Mrázek, Martin Jonás, Jiri Barnat:
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking. CoRR abs/1711.09084 (2017) - 2016
- [j17]Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila:
Analysing sanity of requirements for avionics systems. Formal Aspects Comput. 28(1): 45-63 (2016) - [j16]Petr Rockai, Jiri Barnat, Lubos Brim:
Model checking C++ programs with exceptions. Sci. Comput. Program. 128: 68-85 (2016) - [j15]Petr Bauch, Vojtech Havel, Jiri Barnat:
Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. Softw. Qual. J. 24(1): 37-63 (2016) - [j14]Petr Bauch, Vojtech Havel, Jiri Barnat:
Control Explicit-Data Symbolic Model Checking. ACM Trans. Softw. Eng. Methodol. 25(2): 15:1-15:48 (2016) - [c64]Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerna:
Optimal observation mode scheduling for systems under temporal constraints. ACC 2016: 1099-1104 - [c63]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: 519-531 - [c62]Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat:
Tunable Online MUS/MSS Enumeration. FSTTCS 2016: 50:1-50:13 - [c61]Jiri Barnat, Ivana Cerná, Petr Rockai, Vladimír Still, Kristína Zákopcanová:
On verifying C++ programs with probabilities. SAC 2016: 1238-1243 - [c60]Jaroslav Bendík, Nikola Benes, Jiri Barnat, Ivana Cerná:
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. SEFM 2016: 121-136 - [c59]Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná:
LTL Parameter Synthesis of Parametric Timed Automata. SEFM 2016: 172-187 - [c58]Jan Mrázek, Petr Bauch, Henrich Lauko, Jiri Barnat:
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. SPIN 2016: 208-213 - [c57]Vladimír Still, Petr Rockai, Jiri Barnat:
DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). TACAS 2016: 920-922 - [i7]Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerná:
Optimal Observation Mode Scheduling for Systems under Temporal Constraints. CoRR abs/1602.08260 (2016) - [i6]Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat:
Tunable Online MUS/MSS Enumeration. CoRR abs/1606.03289 (2016) - 2015
- [c56]Vladimír Still, Petr Rockai, Jiri Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations. MEMICS 2015: 144-155 - [c55]Petr Rockai, Vladimír Still, Jiri Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code. SEFM 2015: 268-282 - [c54]Jiri Barnat:
Quo Vadis Explicit-State Model Checking. SOFSEM 2015: 46-57 - [c53]Jiri Barnat, Petr Rockai, Vladimír Still, Jirí Weiser:
Fast, Dynamically-Sized Concurrent Hash Table. SPIN 2015: 49-65 - [i5]Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila:
Analysing Sanity of Requirements for Avionics Systems (Preliminary Version). CoRR abs/1510.02669 (2015) - 2014
- [j13]Petr Rockai, Jiri Barnat, Lubos Brim:
Model Checking C++ with Exceptions. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014) - [c52]Jiri Barnat, Petr Bauch, Vojtech Havel:
Temporal Verification of Simulink Diagrams. HASE 2014: 81-88 - [c51]Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná:
On Clock-Aware LTL Properties of Timed Automata. ICTAC 2014: 43-60 - [c50]Petr Bauch, Vojtech Havel, Jiri Barnat:
LTL Model Checking of LLVM Bitcode with Symbolic Data. MEMICS 2014: 47-59 - [c49]Vladimír Still, Petr Rockai, Jiri Barnat:
Context-Switch-Directed Verification in DIVINE. MEMICS 2014: 135-146 - [c48]Jiri Barnat, Petr Bauch, Vojtech Havel:
Model Checking Parallel Programs with Inputs. PDP 2014: 756-759 - [i4]Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná:
LTL Model Checking of Parametric Timed Automata. CoRR abs/1409.3696 (2014) - 2013
- [j12]Boyan Yordanov, Jana Tumova, Ivana Cerná, Jiri Barnat, Calin Belta:
Formal analysis of piecewise affine systems through formula-guided refinement. Autom. 49(1): 261-266 (2013) - [c47]Jiri Barnat, Lubos Brim, Vojtech Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD 2013: 51-59 - [c46]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: 863-868 - [c45]Jiri Barnat, Nikola Benes, Ivana Cerná, Zuzana Petruchová:
DCCL: verification of component systems with ensembles. CBSE 2013: 43-52 - [c44]Jiri Barnat, Nikola Benes, Tomás Bures, Ivana Cerná, Jaroslav Keznikl, Frantisek Plásil:
Towards Verification of Ensemble-Based Component Systems. FACS 2013: 41-60 - [c43]Petr Rockai, Jiri Barnat, Lubos Brim:
Improved State Space Reductions for LTL Model Checking of C and C++ Programs. NASA Formal Methods 2013: 1-15 - [i3]Jiri Barnat, Petr Bauch:
Control Explicit---Data Symbolic Model Checking: An Introduction. CoRR abs/1303.7379 (2013) - 2012
- [j11]Jiri Barnat, Ivana Cerná, Jana Tumova:
Verification of Systems with Degradation. Comput. Informatics 31(3): 507- (2012) - [j10]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distributed Comput. 72(9): 1083-1097 (2012) - [j9]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): 1272-1288 (2012) - [j8]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): 1491-1504 (2012) - [j7]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): 693-705 (2012) - [c42]María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna:
Attraction-based receding horizon path planning with temporal logic constraints. CDC 2012: 6749-6754 - [c41]Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai:
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. FMICS 2012: 78-92 - [c40]Jiri Barnat, Lubos Brim, Petr Rockai:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NASA Formal Methods 2012: 252-266 - [c39]Jiri Barnat, Petr Bauch, Lubos Brim:
Checking Sanity of Software Requirements. SEFM 2012: 48-62 - [c38]Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira:
Executing Model Checking Counterexamples in Simulink. TASE 2012: 245-248 - [c37]Jiri Barnat, Jan Havlícek, Petr Rockai:
Distributed LTL Model Checking with Hash Compaction. PASM/PDMC 2012: 79-93 - [i2]María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna:
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints. CoRR abs/1208.5855 (2012) - 2011
- [j6]Jiri Barnat, Jakub Chaloupka, Jaco van de Pol:
Distributed Algorithms for SCC Decomposition. J. Log. Comput. 21(1): 23-44 (2011) - [j5]Stefan Edelkamp, Damian Sulewski, Jiri Barnat, Lubos Brim, Pavel Simecek:
Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2): 136-157 (2011) - [c36]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Computing Strongly Connected Components in Parallel on CUDA. IPDPS 2011: 544-555 - [c35]Jiri Barnat, Ivana Cerná, Jana Tumova:
Timed Automata Approach to Verification of Systems with Degradation. MEMICS 2011: 84-93 - [c34]Lubos Brim, Jiri Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century. PDMC 2011: 1-12 - [c33]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Computing Optimal Cycle Mean in Parallel on CUDA. PDMC 2011: 68-83 - [e1]Jiri Barnat, Keijo Heljanko:
Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snowbird, Utah, USA, July 14, 2011. EPTCS 72, 2011 [contents] - 2010
- [j4]Jiri Barnat, Lubos Brim, David Safránek:
High-performance analysis of biological systems dynamics with the DiVinE model checker. Briefings Bioinform. 11(3): 301-312 (2010) - [j3]Jiri Barnat, Lubos Brim, Petr Rockai:
Scalable shared memory LTL model checking. Int. J. Softw. Tools Technol. Transf. 12(2): 139-153 (2010) - [c32]Jana Tumova, Boyan Yordanov, Calin Belta, Ivana Cerna, Jiri Barnat:
A symbolic approach to controlling piecewise affine systems. CDC 2010: 4230-4235 - [c31]Boyan Yordanov, Jana Tumova, Calin Belta, Ivana Cerna, Jiri Barnat:
Formal analysis of piecewise affine systems through formula-guided refinement. CDC 2010: 5899-5904 - [c30]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS 2010: 259-266 - [c29]Jiri Barnat, Lubos Brim, Petr Rockai:
Parallel Partial Order Reduction with Topological Sort Proviso. SEFM 2010: 222-231
2000 – 2009
- 2009
- [j2]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): 3128-3148 (2009) - [c28]Jiri Barnat, Lubos Brim, Petr Rockai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. ICFEM 2009: 407-425 - [c27]Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr:
CUDA Accelerated LTL Model Checking. ICPADS 2009: 34-41 - [c26]Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim:
Efficient large-scale model checking. IPDPS 2009: 1-12 - [c25]Jiri Barnat, Lubos Brim, Pavel Simecek:
Cluster-Based I/O-Efficient LTL Model Checking. ASE 2009: 635-639 - [c24]Jiri Barnat, Ivana Cerná, Jana Tumova:
Quantitative Model Checking of Systems with Degradation. QEST 2009: 21-30 - [c23]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: 31-45 - [c22]Jiri Barnat, Lubos Brim, Milan Ceska:
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. PDMC 2009: 107-111 - 2008
- [c21]Jiri Barnat, Lubos Brim, Petr Rockai:
DiVinE Multi-Core - A Parallel LTL Model-Checker. ATVA 2008: 234-239 - [c20]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
Local Quantitative LTL Model Checking. FMICS 2008: 53-68 - [c19]Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek:
Can Flash Memory Help in Model Checking? FMICS 2008: 150-165 - [c18]Jiri Barnat, Lubos Brim:
Squeeze All the Power Out of Your Hardware to Verify Your Software!. ISoLA 2008: 604-618 - [c17]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. QEST 2008: 77-78 - [c16]Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. TACAS 2008: 48-62 - [i1]Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim:
Efficient Large-Scale Model Checking. Distributed Verification and Grid Computing 2008 - 2007
- [c15]Jiri Barnat, Lubos Brim, Pavel Simecek:
I/O Efficient Accepting Cycle Detection. CAV 2007: 281-293 - [c14]Jiri Barnat, Lubos Brim, Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform. ICECCS 2007: 330-339 - [c13]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
ProbDiVinE: A Parallel Qualitative LTL Model Checker. QEST 2007: 215-216 - [c12]Lubos Brim, Jiri Barnat:
Tutorial: Parallel Model Checking. SPIN 2007: 2-3 - [c11]Jiri Barnat, Lubos Brim, Petr Rockai:
Scalable Multi-core LTL Model-Checking. SPIN 2007: 187-203 - [c10]Jiri Barnat, Lubos Brim, Ivana Cerná, Sven Drazan, David Safránek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. FBTC@CONCUR 2007: 35-50 - [c9]Jiri Barnat, Jakub Chaloupka, Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition. PDMC@CAV 2007: 63-77 - [c8]Jiri Barnat, Petr Rockai:
Shared Hash Tables in Parallel Model Checking. PDMC@CAV 2007: 79-91 - 2006
- [j1]Jiri Barnat, Ivana Cerná:
Distributed breadth-first search LTL model checking. Formal Methods Syst. Des. 29(2): 117-134 (2006) - [c7]Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek:
DiVinE - A Tool for Distributed Verification. CAV 2006: 278-281 - [c6]Jiri Barnat, Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. FMICS/PDMC 2006: 316-330 - 2005
- [c5]Jiri Barnat, Lubos Brim, Ivana Cerná:
Cluster-Based LTL Model Checking of Large Systems. FMCO 2005: 259-279 - 2004
- [c4]Jiri Barnat, Lubos Brim, Jakub Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking. FMICS 2004: 21-39 - 2003
- [c3]