Jiri 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 – today
- 2018
- [j25]Peter Bezdek, Nikola Benes, Ivana Cerná, Jiri Barnat:
On clock-aware LTL parameter synthesis of timed automata. J. Log. Algebr. Meth. Program. 99: 114-142 (2018) - [j24]Petr Rockai, Vladimír Still, Ivana Cerná, Jiri Barnat:
DiVM: Model checking with LLVM and graph memory. Journal of Systems and Software 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]
- [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. Software Quality Journal 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]
- [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]
- [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. Automatica 49(1): 261-266 (2013) - [j17]Jiri Barnat, Jan Havlícek, Petr Rockai:
Distributed LTL Model Checking with Hash Compaction. Electr. 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. Computing and Informatics 31(3): 507- (2012) - [j15]Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska Jr.:
Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distrib. 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. Automat. Contr. 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]
- [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 Jr.:
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 Jr.:
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 in Bioinformatics 11(3): 301-312 (2010) - [j8]Jiri Barnat, Lubos Brim, Petr Rockai:
Scalable shared memory LTL model checking. STTT 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 Jr.:
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 Jr., 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 Jr.:
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. Electr. Notes Theor. Comput. Sci. 194(3): 35-50 (2008) - [j5]Jiri Barnat, Jakub Chaloupka, Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition. Electr. Notes Theor. Comput. Sci. 198(1): 63-77 (2008) - [j4]Jiri Barnat, Petr Rockai:
Shared Hash Tables in Parallel Model Checking. Electr. 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 Jr., 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 Jr., 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]
- [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 Jr., Jana Tumova:
ProbDiVinE: A Parallel Qualitative LTL Model Checker. QEST 2007: 215-216 - [c7]
- [c6]
- 2006
- [j3]Jiri Barnat, Ivana Cerná:
Distributed breadth-first search LTL model checking. Formal Methods in System Design 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. Electr. 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. Electr. 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]
Coauthor Index
last updated on 2019-01-09 01:44 CET by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint