Jiří Barnat

2017

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill:
Model Checking of C and C++ with DIVINE 4,
International Symposium on Automated Technology for Verification and Analysis (ATVA) (to appear), 2017, volume 10482 of Lecture Notes in Computer Science. [bibtex, pdf, url, paper page]

Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, and Jiří Barnat:
Optimizing and Caching SMT Queries in SymDIVINE,
Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, Springer Berlin Heidelberg, 2017, 390–393. [bibtex, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification,
IEEE International Conference on Software Quality, Reliability and Security (QRS), 2017, 54-64. [bibtex, pdf, url, paper page]

2016

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories,
Software Quality Journal, 2016. [bibtex, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
DIVINE: Explicit-State LTL Model Checker,
Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2016, 920–922. [bibtex, pdf, url]

Jaroslav Bendík, Nikola Beneš, Jiří Barnat, and Ivana Černá:
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis,
Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings, 2016, 121–136. [bibtex, url]

Peter Bezděk, Nikola Beneš, Jiří Barnat, and Ivana Černá:
LTL Parameter Synthesis of Parametric Timed Automata,
Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings, 2016, 172–187. [bibtex, url]

Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, and Kristína Zákopčanová:
On Verifying C++ Programs with Probabilities,
ACM Symposium on Applied Computing, 2016, 1238–1243. [bibtex, url]

Jan Mrázek, Petr Bauch, Henrich Lauko, and Jiří Barnat:
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration,
Model Checking Software: 23rd International Symposium, SPIN, Springer International Publishing, 2016, 208–213. [bibtex, pdf, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations,
Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture Notes in Computer Science, 144–155. [bibtex, pdf, url]

2015

Jiří Barnat, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
Fast, Dynamically-Sized Concurrent Hash Table,
Model Checking Software (SPIN 2015), Springer International Publishing, 2015, volume 9232 of Lecture Notes in Computer Science, 49-65. [bibtex, pdf, url]

Jiří Barnat:
Quo Vadis Explicit-State Model Checking,
SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, Springer, 2015, 46-57. [bibtex, url]

Petr Ročkai, Vladimír Štill, and Jiří Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code,
Software Engineering and Formal Methods, Springer International Publishing, 2015, volume 9276 of Lecture Notes in Computer Science, 268–282. [bibtex, pdf, url]

2014

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Context-Switch-Directed Verification in DIVINE,
Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146. [bibtex, pdf, url]

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
LTL Model Checking of LLVM Bitcode with Symbolic Data,
Proceedings of MEMICS’14, Springer, 2014, 47-59. [bibtex, url]

Peter Bezděk, Nikola Beneš, Jiří Barnat, and Ivana Černá:
LTL Model Checking of Parametric Timed Automata,
MEMICS 2014, NOVPRESS, 2014, 28-39. [bibtex]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Model Checking C++ with Exceptions,
Automated Verification of Critical Systems, 2014. [bibtex, url]

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Model Checking Parallel Programs with Inputs,
Parallel, Distributed and Network-Based Processing (PDP), 2014 22nd Euromicro International Conference on, 2014, 756-759. [bibtex, url]

Peter Bezděk, Nikola Beneš, Vojtěch Havel, Jiří Barnat, and Ivana Černá:
On Clock-Aware LTL properties of Timed Automata,
International Colloquium on Theoretical Aspects of Computing (ICTAC), Springer, 2014, volume 8687 of LNCS, 46–60. [bibtex]

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Temporal Verification of Simulink Diagrams,
Proceedings of HASE 2014, IEEE Computer Society, 2014, 81-88. [bibtex]

Jiří Barnat, Nikola Beneš, Tomáš Bureš, Ivana Černá, Jaroslav Keznikl, and František Plášil:
Towards Verification of Ensemble-Based Component Systems,
Formal Aspects of Component Software (FACS), Springer, 2014, volume 8348 of LNCS, 1–20. [bibtex]

2013

Jiří Barnat, Nikola Beneš, Ivana Černá, and Zuzana Petruchová:
DCCL: Verification of Component Systems with Ensembles,
Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, ACM, 2013, 43–52. [bibtex, url]

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868. [bibtex, url]

Jiří Barnat, Jan Havlíček, and Petr Ročkai:
Distributed LTL Model Checking with Hash Compaction,
Electronic Notes in Theoretical Computer Science, Volume 296, Elsevier Science, 2013, 79-93. [bibtex, url]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Formal analysis of piecewise affine systems through formula-guided refinement,
Automatica, 2013, 261–266. [bibtex, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Improved State Space Reductions for LTL Model Checking of C & C++ Programs,
NASA Formal Methods (NFM 2013), Springer, 2013, volume 7871 of LNCS, 1–15. [bibtex]

Jiří Barnat, Luboš Brim, and Vojtěch Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model,
Application of Concurrency to System Design (ACSD), IEEE, 2013, 51–59. [bibtex, url]

2012

Mária Svoreňová, Jana Tůmová, Jiří Barnat, and Ivana Černá:
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints,
IEEE Conference on Decision and Control (CDC 2012), Omnipress for IEEE Control Systems Society, 2012, 6749–6754. [bibtex]

Jiří Barnat, Petr Bauch, and Luboš Brim:
Checking Sanity of Software Requirements,
Software Engineering and Formal Methods: 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 48–62. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Designing Fast LTL Model Checking Algorithms for Many-core GPUs,
Journal of Parallel and Distributed Computing, 2012. [bibtex, url]

Jiří Barnat, Luboš Brim, Jan Beran, Tomáš Kratochvíla, and Italo Romani de Oliveira:
Executing Model Checking Counterexamples in Simulink,
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering, IEEE Computer Society, 2012, 245-248. [bibtex]

Jiří Barnat, Luboš Brim, Adam Krejci, Adam Streck, David Šafránek, Martin Vejnár, and Tomáš Vejpustek:
On Parameter Synthesis by Parallel Model Checking,
IEEE/ACM Trans. Comput. Biol. Bioinformatics, IEEE Computer Society Press, 2012, 693–705. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties,
Science of Computer Programming, Elsevier North-Holland, Inc., 2012, 1272–1288. [bibtex, url]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems,
IEEE Transactions on Automatic Control, 2012. [bibtex, url]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems,
IEEE Transactions on Automatic Control, 2012. [bibtex, url]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Timed Automata Approach to Verification of Systems with Degradation,
MEMICS 2011, Springer, 2012, 84 - 93. [bibtex, url]

Jiří Barnat, Jan Beran, Luboš Brim, Kratochvíla Tomáš, and Ročkai Petr:
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs,
Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 78–92. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs,
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 252–266. [bibtex, url]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Verification of Systems with Degradation,
Computing and Informatics, 2012. [bibtex]

2011

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Computing Optimal Cycle Mean in Parallel on CUDA,
Electronic Proceedings in Theoretical Computer Science, 2011. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Ceška:
Computing Strongly Connected Components in Parallel on CUDA,
Parallel Distributed Processing Symposium (IPDPS), 2011 IEEE International, 2011, 544-555. [bibtex, url]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, 2011. [bibtex, url]

Stefan Edelkamp, Damian Sulewski, Jiří Barnat, Luboš Brim, and Pavel Šimeček:
Flash memory efficient LTL model checking,
Science of Computer Programming, 2011. [bibtex, url]

Luboš Brim and Jiří Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century,
Electronic Proceedings in Theoretical Computer Science, 2011. [bibtex, url]

2010

Jana Tůmová, Boyan Yordanov, Calin Belta, Ivana Černá, and Jiří Barnat:
A Symbolic Approach to Controlling Piecewise Affine Systems,
Proceedings of of the 49th IEEE Conference on Decision and Control (CDC), Omnipress for IEEE Control Systems Society, 2010, 4230 -4235. [bibtex]

Jiří Barnat, Luboš Brim, Milan Češka, and Petr Ročkai:
DiVinE: Parallel Distributed Model Checker,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, 2010, 4–7. [bibtex, url]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, 2010. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking,
16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE, 2010. [bibtex]

Boyan Yordanov, Jana Tůmová, Calin Belta, Ivana Černá, and Jiří Barnat:
Formal Analysis of Piecewise Affine Systems through Formula -Guided Refinement,
Proceedings of of the 49th IEEE Conference on Decision and Control (CDC), Omnipress for IEEE Control Systems Society, 2010, 5899 -5904. [bibtex]

Jiří Barnat, Luboš Brim, and David Šafránek:
High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker,
Briefings in Bioinformatics, 2010, 301–312. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Parallel Partial Order Reduction with Topological Sort Proviso,
Proceeding of SEFM 2010, IEEE Computer Society Press, 2010. [bibtex]

Jiří Barnat, Luboš Brim, David Šafránek, and Martin Vejnár:
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology,
Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010), IEEE, 2010. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Shared Memory LTL Model Checking,
International Journal on Software Tools for Technology Transfer (STTT), 2010, 139–153. [bibtex, url]

2009

Jiří Barnat, Luboš Brim, and Petr Ročkai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties,
Formal Methods and Software Engineering (ICFEM 2009), Springer, 2009, volume 5885 of LNCS, 407–425. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, David Šafránek, and Hongwu Ma:
BioDiVinE: A Framework for Parallel Analysis of Biological Models,
Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), 2009, 31–45. [bibtex, url]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, and David Šafránek:
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models,
Proceedings of The 7th Conference on Computational Methods in Systems Biology (CMSB’09), Universita di Pisa, 2009, volume TR-09-09 of Technical Report, 1–5. [bibtex]

Jiří Barnat, Luboš Brim, Milan Češka, and Tomáš Lamr:
CUDA accelerated LTL Model Checking,
15th International Conference on Parallel and Distributed Systems (ICPADS 2009), IEEE Computer Society, 2009, 34–41. [bibtex]

Jiří Barnat, Luboš Brim, and Pavel Šimeček:
Cluster-Based I/O Efficient LTL Model Checking,
24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), IEEE Computer Society, 2009, 635–639. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, and David Šafránek:
Computational Analysis of Large-Scale Multi-Affine ODE Models,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 81–90. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE 2.0: High-Performance Model Checking,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 31–32. [bibtex]

Jiří Barnat, Luboš Brim, and Milan Češka:
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking,
Electronic Proceedings in Theoretical Computer Science (PDMC 2009), 2009, 107–111. [bibtex, url]

Kees Verstoep, Henri Bal, Jiří Barnat, and Luboš Brim:
Efficient Large-Scale Model Checking,
23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009), IEEE, 2009. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
Local Quantitative LTL Model Checking,
Formal Methods for Industrial Critical Systems, Springer Berlin / Heidelberg, 2009, 53-68. [bibtex, url]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, and David Šafránek:
On algorithmic analysis of transcriptional regulation by LTL model checking,
Theor. Comput. Sci., 2009, 3128–3148. [bibtex, url]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Quantitative Model Checking of Systems with Degradation,
Proceeding of the Sixth International Conference on Quantitative Evaluation of Systems (QEST 2009), IEEE, 2009, 21–30. [bibtex]

2008

Jiří Barnat, Luboš Brim, Stefan Edelkamp, Damian Sulewski, and Pavel Šimeček:
Can Flash Memory Help in Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 150–165. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE Multi-Core – A Parallel LTL Model-Checker,
Automated Technology for Verification and Analysis (ATVA 2008), Springer, 2008, volume 5311 of LNCS, 234–239. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks,
Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation, Ivana Černá and Gerald Luettgen, 2008, 83-96. [bibtex]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition,
ENTCS, 2008, 63–77. [bibtex]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers B. V., 2008, 63–77. [bibtex, url]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
Local Quantitative LTL Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 53–68. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE,
ENTCS, Elsevier, 2008, volume 194 of ENTCS, 35–50. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems,
QEST ’08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, IEEE Computer Society, 2008, 77–78. [bibtex, url]

Jiří Barnat, Luboš Brim, Pavel Šimeček, and Michael Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking,
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)., Springer, 2008, volume 4963 of LNCS, 48–62. [bibtex]

Jiří Barnat and Petr Ročkai:
Shared Hash Tables in Parallel Model Checking,
ENTCS, 2008, 79–91. [bibtex]

Luboš Brim and Jiří Barnat:
Squeeze All the Power Out of Your Hardware to Verify Your Software!,
ISOLA 2008, Springer Verlag, 2008, volume 17 of CCIS, 604–618. [bibtex]

2007

Jiří Barnat, Luboš Brim, and Pavel Šimeček:
I/O Efficient Accepting Cycle Detection,
Computer Aided Verification, Springer, 2007, volume 4590 of LNCS, 281–293. [bibtex]

Jiří Barnat, Luboš Brim, and Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform,
The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society Press, 2007. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
Parallel Model-Checking Genetic Regulatory Networks,
Towards Systems Biology, Verimag, 2007. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
ProbDiVinE: A Parallel Qualitative LTL Model Checker,
Fourth International Conference on the Quantitative Evaluation of Systems (QEST’07), IEEE Computer Society, 2007, 215–216. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Multi-core LTL Model-Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 187–203. [bibtex]

Luboš Brim and Jiří Barnat:
Tutorial: Parallel Model Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 2–3. [bibtex]

2006

Jiří Barnat, Luboš Brim, and Ivana Černá:
Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, Springer, 2006, 259-279. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai, and Pavel Šimeček:
DiVinE – A Tool for Distributed Verification (Tool Paper),
Computer Aided Verification, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278–281. [bibtex]

Jiří Barnat and Ivana Černá:
Distributed Breadth-First Search LTL Model Checking,
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, 2006, 117–134(18). [bibtex]

Jiří Barnat and Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs,
Formal Methods: Applications and Technology, Springer, 2006, volume 4346 of LNCS, 316–330. [bibtex]

2005

Jiří Barnat, Luboš Brim, and Ivana Černá:
Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, 2005, 259–279. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, and Pavel Šimeček:
DiVinE The Distributed Verification Environment,
4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’05), 2005. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, and Pavel Šimeček:
DiVinE – The Distributed Verification Environment,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 89–94. [bibtex]

Jiří Barnat, Vojěch Forejt, Martin Leucker, and Michael Weber:
DivSPIN – A SPIN compatible distributed model checker,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 95–100. [bibtex]

Jiří Barnat, Luboš Brim, and Jakub Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2005, 21–39. [bibtex]

2004

Jiří Barnat:
Distributed Memory LTL Model Checking,
2004. [bibtex]

2003

Luboš Brim and Jiří Barnat:
Distribution of Explicit-State LTL Model-Checking,
8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science. [bibtex]

Jiří Barnat, Luboš Brim, and Jakub Chaloupka:
Parallel Breadth-First Search LTL Model-Checking,
18th IEEE International Conference on Automated Software Engineering (ASE’03), IEEE Computer Society, 2003, 106–115. [bibtex]

2002

Jiří Barnat:
How to Distribute LTL Model-checking Using Decomposition of Negative Claim Automaton,
SOFSEM 2002 Student Research Forum, 2002, 9–14. [bibtex]

Jiří Barnat, Tomáš Brázdil, Pavel Krčál, Vojtěch Řehák, and David Šafránek:
Model Checking in IPv6 Hardware Router Design,
2002, 8. [bibtex]

Jiří Barnat, Luboš Brim, and Ivana Černá:
Property Driven Distribution of Nested DFS,
Proceeding of the 3rd International Workshop on Verification and Computational Logic (VCL’2002), 2002, 1–10. [bibtex]

Jiří Barnat, Luboš Brim, and Ivana Černá:
Property driven distribution of Nested DFS,
Proc. Workshop on Verification and Computational Logic, 2002, 1–10. [bibtex]

2001

Jiří Barnat, Luboš Brim, and Jitka Stříbrná:
Distributed LTL Model-Checking in SPIN,
Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume 2057 of LNCS, 200–216. [bibtex]