Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarJiri 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
2010 – 2019
- 2019
[c70]Petr Rockai, Jiri Barnat:
A Simulator for LLVM Bitcode. FMICS 2019: 127-142- [c69]Jan Mrázek, Jiri Barnat:
RoFICoM - First Open-Hardware Connector for Metamorphic Robots. IROS 2019: 2720-2725 - [c68]Petr Rockai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiri Barnat:
Reproducible Execution of POSIX Programs with DiOS. SEFM 2019: 333-349 - [c67]Vladimír Still, Jiri Barnat:
Local Nontermination Detection for Parallel C++ Programs. SEFM 2019: 373-390 - [c66]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
- [j25]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) - [j24]Petr Rockai
, Vladimír Still, Ivana Cerná, Jiri Barnat:
DiVM: Model checking with LLVM and graph memory. J. Syst. Softw. 143: 1-13 (2018) - [c65]Vladimír Still, Jiri Barnat:
Model Checking of C++ Programs Under the x86-TSO Memory Model. ICFEM 2018: 124-140 - [c64]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
- [c63]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 - [c62]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 - [c61]Vladimír Still, Petr Rockai, Jiri Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification. QRS 2017: 54-64 - [c60]Katarína Kejstová, Petr Rockai, Jiri Barnat:
From Model Checking to Runtime Verification and Back. RV 2017: 225-240 - [c59]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
- [j23]Jiri Barnat, Petr Bauch, Nikola Benes, Lubos Brim, Jan Beran, Tomas Kratochvila:
Analysing sanity of requirements for avionics systems. Formal Asp. Comput. 28(1): 45-63 (2016) - [j22]Petr Rockai, Jiri Barnat, Lubos Brim:
Model checking C++ programs with exceptions. Sci. Comput. Program. 128: 68-85 (2016) - [j21]Petr Bauch, Vojtech Havel, Jiri Barnat:
Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. Softw. Qual. J. 24(1): 37-63 (2016) - [j20]Petr Bauch, Vojtech Havel, Jiri Barnat:
Control Explicit-Data Symbolic Model Checking. ACM Trans. Softw. Eng. Methodol. 25(2): 15:1-15:48 (2016) - [c58]Eva Tesarova, María Svorenová, Jiri Barnat, Ivana Cerna:
Optimal observation mode scheduling for systems under temporal constraints. ACC 2016: 1099-1104 - [c57]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 - [c56]Jaroslav Bendík, Nikola Benes, Ivana Cerná, Jiri Barnat:
Tunable Online MUS/MSS Enumeration. FSTTCS 2016: 50:1-50:13 - [c55]Jiri Barnat, Ivana Cerná, Petr Rockai, Vladimír Still, Kristína Zákopcanová:
On verifying C++ programs with probabilities. SAC 2016: 1238-1243 - [c54]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 - [c53]Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cerná:
LTL Parameter Synthesis of Parametric Timed Automata. SEFM 2016: 172-187 - [c52]Jan Mrázek, Petr Bauch, Henrich Lauko, Jiri Barnat:
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. SPIN 2016: 208-213 - [c51]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
- [c50]Vladimír Still, Petr Rockai, Jiri Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations. MEMICS 2015: 144-155 - [c49]Petr Rockai, Vladimír Still, Jiri Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code. SEFM 2015: 268-282 - [c48]Jiri Barnat:
Quo Vadis Explicit-State Model Checking. SOFSEM 2015: 46-57 - [c47]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
- [j19]Petr Rockai, Jiri Barnat, Lubos Brim:
Model Checking C++ with Exceptions. ECEASST 70 (2014) - [c46]Jiri Barnat, Petr Bauch, Vojtech Havel:
Temporal Verification of Simulink Diagrams. HASE 2014: 81-88 - [c45]Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cerná:
On Clock-Aware LTL Properties of Timed Automata. ICTAC 2014: 43-60 - [c44]Petr Bauch, Vojtech Havel, Jiri Barnat:
LTL Model Checking of LLVM Bitcode with Symbolic Data. MEMICS 2014: 47-59 - [c43]Vladimír Still, Petr Rockai, Jiri Barnat:
Context-Switch-Directed Verification in DIVINE. MEMICS 2014: 135-146 - [c42]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
- [j18]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) - [j17]Jiri Barnat, Jan Havlícek, Petr Rockai:
Distributed LTL Model Checking with Hash Compaction. Electron. Notes Theor. Comput. Sci. 296: 79-93 (2013) - [c41]Jiri Barnat, Lubos Brim, Vojtech Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD 2013: 51-59 - [c40]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 - [c39]Jiri Barnat, Nikola Benes, Ivana Cerná, Zuzana Petruchová:
DCCL: verification of component systems with ensembles. CBSE 2013: 43-52 - [c38]Jiri Barnat, Nikola Benes, Tomás Bures, Ivana Cerná, Jaroslav Keznikl, Frantisek Plasil:
Towards Verification of Ensemble-Based Component Systems. FACS 2013: 41-60 - [c37]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
- [j16]Jiri Barnat, Ivana Cerná, Jana Tumova:
Verification of Systems with Degradation. Comput. Informatics 31(3): 507- (2012) - [j15]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) - [j14]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) - [j13]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) - [j12]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. Biology Bioinform. 9(3): 693-705 (2012) - [c36]María Svorenová, Jana Tumova, Jiri Barnat, Ivana Cerna:
Attraction-based receding horizon path planning with temporal logic constraints. CDC 2012: 6749-6754 - [c35]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 - [c34]Jiri Barnat, Lubos Brim, Petr Rockai:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NASA Formal Methods 2012: 252-266 - [c33]Jiri Barnat, Petr Bauch, Lubos Brim:
Checking Sanity of Software Requirements. SEFM 2012: 48-62 - [c32]Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira:
Executing Model Checking Counterexamples in Simulink. TASE 2012: 245-248 - [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
- [j11]Jiri Barnat, Jakub Chaloupka, Jaco van de Pol:
Distributed Algorithms for SCC Decomposition. J. Log. Comput. 21(1): 23-44 (2011) - [j10]Stefan Edelkamp, Damian Sulewski, Jiri Barnat, Lubos Brim, Pavel Simecek:
Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2): 136-157 (2011) - [c31]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Computing Strongly Connected Components in Parallel on CUDA. IPDPS 2011: 544-555 - [c30]Jiri Barnat, Ivana Cerná, Jana Tumova:
Timed Automata Approach to Verification of Systems with Degradation. MEMICS 2011: 84-93 - [c29]Lubos Brim, Jiri Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century. PDMC 2011: 1-12 - [c28]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
- [j9]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) - [j8]Jiri Barnat, Lubos Brim, Petr Rockai:
Scalable shared memory LTL model checking. Int. J. Softw. Tools Technol. Transf. 12(2): 139-153 (2010) - [c27]Jana Tumova, Boyan Yordanov, Calin Belta, Ivana Cerna, Jiri Barnat:
A symbolic approach to controlling piecewise affine systems. CDC 2010: 4230-4235 - [c26]Boyan Yordanov, Jana Tumova, Calin Belta, Ivana Cerna, Jiri Barnat:
Formal analysis of piecewise affine systems through formula-guided refinement. CDC 2010: 5899-5904 - [c25]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS 2010: 259-266 - [c24]Jiri Barnat, Lubos Brim, Petr Rockai:
Parallel Partial Order Reduction with Topological Sort Proviso. SEFM 2010: 222-231
2000 – 2009
- 2009
- [j7]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) - [c23]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 - [c22]Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr:
CUDA Accelerated LTL Model Checking. ICPADS 2009: 34-41 - [c21]Kees Verstoep, Henri E. Bal, Jiri Barnat, Lubos Brim:
Efficient large-scale model checking. IPDPS 2009: 1-12 - [c20]Jiri Barnat, Lubos Brim, Pavel Simecek:
Cluster-Based I/O-Efficient LTL Model Checking. ASE 2009: 635-639 - [c19]Jiri Barnat, Ivana Cerná, Jana Tumova:
Quantitative Model Checking of Systems with Degradation. QEST 2009: 21-30 - [c18]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 - [c17]Jiri Barnat, Lubos Brim, Milan Ceska:
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. PDMC 2009: 107-111 - 2008
- [j6]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): 35-50 (2008) - [j5]Jiri Barnat, Jakub Chaloupka, Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition. Electron. Notes Theor. Comput. Sci. 198(1): 63-77 (2008) - [j4]Jiri Barnat, Petr Rockai:
Shared Hash Tables in Parallel Model Checking. Electron. Notes Theor. Comput. Sci. 198(1): 79-91 (2008) - [c16]Jiri Barnat, Lubos Brim, Petr Rockai:
DiVinE Multi-Core - A Parallel LTL Model-Checker. ATVA 2008: 234-239 - [c15]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
Local Quantitative LTL Model Checking. FMICS 2008: 53-68 - [c14]Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek:
Can Flash Memory Help in Model Checking? FMICS 2008: 150-165 - [c13]Jiri Barnat, Lubos Brim:
Squeeze All the Power Out of Your Hardware to Verify Your Software!. ISoLA 2008: 604-618 - [c12]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. QEST 2008: 77-78 - [c11]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
- [c10]Jiri Barnat, Lubos Brim, Pavel Simecek:
I/O Efficient Accepting Cycle Detection. CAV 2007: 281-293 - [c9]Jiri Barnat, Lubos Brim, Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform. ICECCS 2007: 330-339 - [c8]Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
ProbDiVinE: A Parallel Qualitative LTL Model Checker. QEST 2007: 215-216 - [c7]Lubos Brim, Jiri Barnat:
Tutorial: Parallel Model Checking. SPIN 2007: 2-3 - [c6]Jiri Barnat, Lubos Brim, Petr Rockai:
Scalable Multi-core LTL Model-Checking. SPIN 2007: 187-203 - 2006
- [j3]Jiri Barnat, Ivana Cerná:
Distributed breadth-first search LTL model checking. Formal Methods Syst. Des. 29(2): 117-134 (2006) - [c5]Jiri Barnat, Lubos Brim, Ivana Cerná, Pavel Moravec, Petr Rockai, Pavel Simecek:
DiVinE - A Tool for Distributed Verification. CAV 2006: 278-281 - [c4]Jiri Barnat, Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. FMICS/PDMC 2006: 316-330 - 2005
- [j2]Jiri Barnat, Lubos Brim, Jakub Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electron. Notes Theor. Comput. Sci. 133: 21-39 (2005) - [c3]Jiri Barnat, Lubos Brim, Ivana Cerná:
Cluster-Based LTL Model Checking of Large Systems. FMCO 2005: 259-279 - 2003
- [j1]Lubos Brim, Jiri Barnat:
Distribution of Explicit-State LTL Model-Checking. Electron. Notes Theor. Comput. Sci. 80: 273-278 (2003) - [c2]Jiri Barnat, Lubos Brim, Jakub Chaloupka:
Parallel Breadth-First Search LTL Model-Checking. ASE 2003: 106-115 - 2001
- [c1]Jiri Barnat, Lubos Brim, Jitka Stríbrná:
Distributed LTL Model-Checking in SPIN. SPIN 2001: 200-216
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org and opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy.
Tweets on dblp homepage
Show tweets from 
on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-06-17 01:03 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
