BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008, s. 234-239. ISBN 978-3-540-88386-9.
BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla: ERCIM, 2008, s. 63-78. ISBN 978-3-642-03239-4.
BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. In QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems. Washington, DC, USA: IEEE Computer Society, 2008, s. 77-78. ISBN 978-0-7695-3360-5.
BARNAT, Jiří a Luboš BRIM. Squeeze All the Power Out of Your Hardware to Verify Your Software! In Leveraging Applications of Formal Methods, Verification and Validation. Berlin Heidelberg: Springer, 2008, s. 604-618. ISBN 978-3-540-88478-1.
BARNAT, Jiří a Ivana ČERNÁ. Distributed breadth-first search LTL model checking. Formal Methods in System Design. Springer Netherlands, 2006, roč. 29, č. 2, s. 117-134. ISSN 0925-9856.
BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Distributed Qualitative LTL Model Checking of Markov Decision Processes. In Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation. Bonn, Germany: University of Bonn, 2006, s. 1-15. ISSN 1571-0661.
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electronic Notes in Theoretical Computer Science. Nizozemsko: Elsevier, 2006, roč. 135, č. 2, s. 3-18, 15 s. ISSN 1571-0661.
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. On Combining Partial Order Reduction with Fairness Assumptions. In Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006). Bonn, Germany: University Bonn, 2006, s. 1-16. ISBN 978-3-540-70951-0.
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronical Notes in Theoretical Computer Science. Elsevier, 2005, roč. 2005, č. 133, s. 21-39, 10 s. ISSN 1571-0661.
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005). Lisboa, Portugal: TU Munchen, 2005, s. 1-12.
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. In Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004). Linz, Austria: Institute for Systems Engineering & Automation, Kepler university Linz, 2004, s. 17-34. ISBN 3-902457-03-1.
MORAVEC, Pavel. Using Accepting Predecessors in Distributed LTL Model-Checking. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes. Bruxelles, Belgium: Universite Libre de Bruxelles, 2004, s. 122-129, 7 s.
KRČÁL, Pavel. Distributed Explicit Bounded LTL Model Checking. In Second International Workshop on Parallel and Distributed Model Checking. 89. vyd. Neuveden: Elsevier, 2003, s. 30-47.