Výpis publikací

BENEŠ, Nikola, Luboš BRIM, Ondřej HUVAR, Samuel PASTVA a David ŠAFRÁNEK. Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures. Springer Cham, 2025. ISBN 978-3-031-78708-9.

BENEŠ, Nikola, Luboš BRIM, Ondřej HUVAR, Samuel PASTVA a David ŠAFRÁNEK. BNClassifier: Classifying Boolean Models by Dynamic Properties. Online. In Gori, Roberta; Milazzo, Paolo; Tribastone, Mirco. Computational Methods in Systems Biology. Cham: Springer, 2024, s. 19-26. ISBN 978-3-031-71670-6. Dostupné z: https://dx.doi.org/10.1007/978-3-031-71671-3_2.

BENEŠ, Nikola, Luboš BRIM, Ondřej HUVAR, Samuel PASTVA a David ŠAFRÁNEK. Boolean network sketches: a unifying framework for logical model inference. Bioinformatics. 2023, roč. 39, č. 4, s. "btad158", 8 s. ISSN 1367-4803. Dostupné z: https://dx.doi.org/10.1093/bioinformatics/btad158.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA, David ŠAFRÁNEK a Eva ŠMIJÁKOVÁ. Phenotype Control of Partially Specified Boolean Networks. In Jun Pang, Joachim Niehren. Computational Methods in Systems Biology. Luxembourg City, Luxembourg: Springer Cham, 2023, s. 18-35. ISBN 978-3-031-42696-4. Dostupné z: https://dx.doi.org/10.1007/978-3-031-42697-1_2.

TROJÁK, Matej, David ŠAFRÁNEK, Samuel PASTVA a Luboš BRIM. Rule-based Modelling of Biological Systems Using Regulated Rewriting. Biosystems. Elsevier, 2023, roč. 225, č. 104843, s. 1-15. ISSN 0303-2647. Dostupné z: https://dx.doi.org/10.1016/j.biosystems.2023.104843.

BRIM, Luboš, Samuel PASTVA, David ŠAFRÁNEK a Eva ŠMIJÁKOVÁ. Temporary and Permanent Control of Partially Specified Boolean Networks. BIOSYSTEMS. Elsevier, 2023, roč. 223, JAN, s. 104795-104808. ISSN 0303-2647. Dostupné z: https://dx.doi.org/10.1016/j.biosystems.2022.104795.

BENEŠ, Nikola, Luboš BRIM, Ondřej HUVAR, Samuel PASTVA, David ŠAFRÁNEK a Eva ŠMIJÁKOVÁ. AEON.py: Python library for attractor analysis in asynchronous Boolean networks. BIOINFORMATICS. UK: OXFORD UNIV PRESS, 2022, roč. 38, č. 21, s. 4978-4980. ISSN 1367-4803. Dostupné z: https://dx.doi.org/10.1093/bioinformatics/btac624.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. Logical Methods in Computer Science. Episciences, 2022, roč. 18, č. 1, s. 1-27. ISSN 1860-5974. Dostupné z: https://dx.doi.org/10.46298/LMCS-18(1:38)2022.

TROJÁK, Matej, David ŠAFRÁNEK, Branislav BROZMANN a Luboš BRIM. eBCSgen 2.0: Modelling and Analysis of Regulated Rule-Based Systems. Online. In I. Petre, A. Păun. 20th International Conference on Computational Methods in Systems Biology. LNBI 13447. Neuveden: Springer, 2022, s. 302-309. ISBN 978-3-031-15033-3. Dostupné z: https://dx.doi.org/10.1007/978-3-031-15034-0_17.

BENEŠ, Nikola, Luboš BRIM, Jakub KADLECAJ, Samuel PASTVA a David ŠAFRÁNEK. Exploring attractor bifurcations in Boolean networks. BMC Bioinformatics. 2022, roč. 23, č. 173, s. 1-18. ISSN 1471-2105. Dostupné z: https://dx.doi.org/10.1186/s12859-022-04708-9.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Aeon 2021: Bifurcation Decision Trees in Boolean Networks. In Cinquemani et al. International Conference on Computational Methods in Systems Biology (CMSB 2021). Cham: Springer, 2021, s. 230-237. ISBN 978-3-030-85632-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-85633-5_14.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Computing Bottom SCCs Symbolically Using Transition Guided Reduction. Online. In Alexandra Silva, K. Rustan, M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021. Neuveden: Springer Nature, 2021, s. 505-528. ISBN 978-3-030-81684-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-81685-8_24.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Symbolic Coloured SCC Decomposition. Online. In Jan Friso Groote, Kim Larsen. Tools and Algorithms for the Construction and Analysis of Systems, 27th International Conference, TACAS 2021. Neuveden: Springer Nature, 2021, s. 64-83. ISBN 978-3-030-72012-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-72013-1_4.

BENEŠ, Nikola, Luboš BRIM, Jakub KADLECAJ, Samuel PASTVA a David ŠAFRÁNEK. AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification. CAV 2020. LNCS 12224. Cham: Springer, Cham, 2020, s. 569-581. ISBN 978-3-030-53287-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53288-8_28.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Digital Bifurcation Analysis of Internet Congestion Control Protocols. International Journal of Bifurcation and Chaos. 2020, roč. 30, č. 13, s. 2030038-2030055. ISSN 0218-1274. Dostupné z: https://dx.doi.org/10.1142/S0218127420300384.

TROJÁK, Matej, David ŠAFRÁNEK, Lukrécia MERTOVÁ a Luboš BRIM. eBCSgen: A Software Tool for Biochemical Space Language. Online. In Abate A., Petrov T., Wolf V. 18th International Conference on Computational Methods in Systems Biology, CMSB 2020. LNBI 12314. Neuveden: Springer, 2020, s. 356-361. ISBN 978-3-030-60326-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-60327-4_20.

TROJÁK, Matej, David ŠAFRÁNEK, Lukrécia MERTOVÁ a Luboš BRIM. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. PLOS ONE. Public Library of Science, 2020, roč. 15, č. 9, s. 1-23, 24 s. ISSN 1932-6203. Dostupné z: https://dx.doi.org/10.1371/journal.pone.0238838.

TROJÁK, Matej, David ŠAFRÁNEK, Luboš BRIM, Jakub ŠALAGOVIČ a Jan ČERVENÝ. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. Online. In Ankit Gupta, Tatjana Petrov. 9th International Workshop on Static Analysis and Systems Biology (SASB). ENTCS 350. Amsterdam: Elsevier, 2020, s. 91-116. ISSN 1571-0661. Dostupné z: https://dx.doi.org/10.1016/j.entcs.2020.06.006.

TROJÁK, Matej, David ŠAFRÁNEK, Lukrécia MERTOVÁ a Luboš BRIM. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. In 7th Workshop on Hybrid Systems and Biology. 2020.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Parallel parameter synthesis algorithm for hybrid CTL. Science of Computer Programming. 2020, roč. 185, č. 102321, s. 1-19. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2019.102321.

ŠMIJÁKOVÁ, Eva, Samuel PASTVA, David ŠAFRÁNEK a Luboš BRIM. Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications. Online. In Abate A., Petrov T., Wolf V. Computational Methods in Systems Biology. CMSB 2020. Lecture Notes in Computer Science, vol 12314. Cham: Springer, Cham, 2020, s. 280-297. ISBN 978-3-030-60326-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-60327-4_15.

TROJÁK, Matej, David ŠAFRÁNEK, Lukrécia MERTOVÁ a Luboš BRIM. Parameter Synthesis and Robustness Analysis of Rule-Based Models. In Ritchie Lee, Susmit Jha, Anastasia Mavridou. 12th International Symposium on NASA Formal Methods, NFM 2020. LNCS 12229. Moffett Field, CA, USA: Springer, 2020, s. 41-59. ISBN 978-3-030-55753-9. Dostupné z: https://dx.doi.org/10.1007/978-3-030-55754-6_3.

BENEŠ, Nikola, Luboš BRIM, Martin GELETKA, Samuel PASTVA a David ŠAFRÁNEK. Accelerating Parameter Synthesis Using Semi-algebraic Constraints. Online. In Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth. Integrated Formal Methods. LNCS 11918. Cham: Springer International Publishing, 2019, s. 27-45. ISBN 978-3-030-34967-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-34968-4_2.

ŠAFRÁNEK, David, Matej TROJÁK, Vojtěch BRŮŽA, Tomáš VEJPUSTEK, Jan PAPOUŠEK, Martin DEMKO, Samuel PASTVA, Aleš PEJZNOCH a Luboš BRIM. Barbaric Robustness Monitoring Revisited for STL* in Parasim. In Bortolussi L., Sanguinetti G. Computational Methods in Systems Biology (CMSB 2019). LNBI 11773. Neuveden: Springer, 2019, s. 356-359. ISBN 978-3-030-31303-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31304-3_26.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Digital Bifurcation Analysis of TCP Dynamics. In Tomáš Vojnar and Lijun Zhang. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019. LNCS, volume 11428. Cham: Springer International Publishing, 2019, s. 339-356. ISBN 978-3-030-17464-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-17465-1_19.

BENEŠ, Nikola, Luboš BRIM, Jana DRAŽANOVÁ, Samuel PASTVA a David ŠAFRÁNEK. Facetal Abstraction for Non-linear Dynamical Systems Based on delta-decidable SMT. In Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control. New York, NY, USA: ACM, 2019, s. 99-108. ISBN 978-1-4503-6282-5. Dostupné z: https://dx.doi.org/10.1145/3302504.3311793.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA, Jakub POLÁČEK a David ŠAFRÁNEK. Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks. In Ait Ameur et al. Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings. Heidelberg: Springer, 2019, s. 353-369. ISBN 978-3-030-32408-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32409-4_22.

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. Model Checking Approach to the Analysis of Biological Systems. Online. In Pietro Liò, Paolo Zuliani. Automated Reasoning for Systems Biology and Medicine. Cham: Springer, Cham, 2019, s. 3-35. Computational Biology. ISBN 978-3-030-17296-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-17297-8_1.

BENEŠ, Nikola, Luboš BRIM, Jan ČERVENÝ, Samuel PASTVA, David ŠAFRÁNEK, Jakub ŠALAGOVIČ a Matej TROJÁK. Fully Automated Attractor Analysis of Cyanobacteria Models. In Marian Barbu, Răzvan Şolea, Adrian Filipescu. 22nd International Conference on System Theory, Control and Computing. Neuveden: IEEE, 2018, s. 354-359. ISBN 978-1-5386-4444-7. Dostupné z: https://dx.doi.org/10.1109/ICSTCC.2018.8540762.

DEMKO, Martin, Samuel PASTVA, David ŠAFRÁNEK, Nikola BENEŠ a Luboš BRIM. PITHYA. 2018.

BRIM, Luboš, Jiří BARNAT, David ŠAFRÁNEK, Nikola BENEŠ, Martin DEMKO, Samuel PASTVA a Matej HAJNAL. Detecting Attractors in Biological Models with Uncertain Parameters. In Jérôme Feret and Heinz Koeppl. Computational Methods in Systems Biology. CMSB 2017. LNCS 10545. Cham: Springer International Publishing, 2017, s. 40-56. ISBN 978-3-319-67470-4. Dostupné z: https://dx.doi.org/10.1007/978-3-319-67471-1_3.

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Matej HAJNAL, Samuel PASTVA a David ŠAFRÁNEK. Discrete Bifurcation Analysis with Pithya. In Feret J. et al. 15th International Conference on Computational Methods in Systems Biology (CMSB). LNCS 10545. Cham: Springer, 2017, s. 319-320. ISBN 978-3-319-67470-4.

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, David ŠAFRÁNEK, Samuel PASTVA a Matej HAJNAL. Model Checking Approach to Discrete Bifurcation Analysis. In Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2017.

BRIM, Luboš, David ŠAFRÁNEK, Nikola BENEŠ, Martin DEMKO, Samuel PASTVA a Matej HAJNAL. Parameter Synthesis of Biological Models by Model Checking: A Case Study. In 4th International Synthetic & Systems Biology Summer School. SSBSS 2017. 2017.

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. In Rupak Majumdar and Viktor Kunčak. Computer Aided Verification. CAV 2017. LNCS 10426. Cham: Springer International Publishing, 2017, s. 591-598. ISBN 978-3-319-63386-2. Dostupné z: https://dx.doi.org/10.1007/978-3-319-63387-9_29.

BRIM, Luboš, Nikola BENEŠ, David ŠAFRÁNEK, Martin DEMKO, Samuel PASTVA a Matej HAJNAL. PITHYA: High-Performance Parameter Synthesis for Biological Models. In Intelligent Systems for Molecular Biology and European Conference on Computational Biology. ISMB/ECCB 2017. 2017.

ČEŠKA, Milan, Frits DANNENBERG, Nicola PAOLETTI, Marta KWIATKOWSKA a Luboš BRIM. Precise parameter synthesis for stochastic biochemical systems. Acta informatica. Berlin: Springer-Verlag, 2017, roč. 54, č. 6, s. 589-623. ISSN 0001-5903. Dostupné z: https://dx.doi.org/10.1007/s00236-016-0265-2.

ČEŠKA, Milan, Frits DANNENBERG, Marta KWIATKOWSKA a Luboš BRIM. Precise parameter synthesis for stochastic biochemical systems. Acta informatica. Springer, 2017, roč. 54, č. 6, s. 589-623. ISSN 0001-5903. Dostupné z: https://dx.doi.org/10.1007/s00236-016-0265-2.

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. A Model Checking Approach to Discrete Bifurcation Analysis. In John S. Fitzgerald et al. Formal Methods. FM 2016. LNCS 9995. Neuveden: Springer International Publishing, 2016, s. 85-101. ISBN 978-3-319-48988-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-48989-6_6.

BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN a Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing. 2016, roč. 28, č. 1, s. 45-63. ISSN 0934-5043. Dostupné z: https://dx.doi.org/10.1007/s00165-015-0348-9.

DĚD, Tadeáš, David ŠAFRÁNEK, Matej TROJÁK, Matej KLEMENT, Jakub ŠALAGOVIČ a Luboš BRIM. Formal Biochemical Space with Semantics in Kappa and BNGL. Online. In Loic Pauleve et al. The 6th International Workshop on Static Analysis and Systems Biology, SASB 2015. ENTCS 326. Neuveden: Elsevier, 2016, s. 27-49. ISSN 1571-0661. Dostupné z: https://dx.doi.org/10.1016/j.entcs.2016.09.017.

DEMKO, Martin, Nikola BENEŠ, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. In Ezio Bartocci et al. Computational Methods in Systems Biology. CMSB 2016. LNBI 9859. Neuveden: Springer International Publishing, 2016, s. 82-97. ISBN 978-3-319-45176-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-45177-0_6.

ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, roč. 128, 15 October 2016, s. 68-85. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2016.05.007.

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. In Cyrille Artho et al. Automated Technology for Verification and Analysis. ATVA 2016. LNCS 9938. Neuveden: Springer International Publishing, 2016, s. 192-208. ISBN 978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3_13.

ČEŠKA, Milan, Petr PILAŘ, Nikola PAOLETTI, Luboš BRIM a Marta KWIATKOWSKA. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In Marsha Chechik, Jean-François Raskin. 22nd International Conference, TACAS 2016. LNCS 9636. Berlin: Springer International Publishing, 2016, s. 367-384. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_21.

HAJNAL, Matej, David ŠAFRÁNEK, Martin DEMKO, Samuel PASTVA, Pavel KREJČÍ a Luboš BRIM. Toward Modelling and Analysis of Transient and Sustained Behaviour of Signalling Pathways. In Eugenio Cinquemani. Hybrid Systems Biology. HSB 2016. LNBI 9957. Neuveden: Springer International Publishing, 2016, s. 57-66. ISBN 978-3-319-47150-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-47151-8_4.

ABATE, Alessandro, Milan ČEŠKA, Luboš BRIM a Marta KWIATKOWSKA. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. In 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings. LNCS 9206. Berlin: Springer International Publishing, 2015, s. 195-213. ISBN 978-3-319-21689-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-21690-4_12.

TROJÁK, Matej, Tadeáš DĚD, David ŠAFRÁNEK, Matej KLEMENT, Jan ČERVENÝ a Luboš BRIM. Biochemical Space: A Language for Formal Description and Annotation of Complex Biological Processes. In 13th Conference on Computational Methods in Systems Biology. 2015.

TROJÁK, Matej, David ŠAFRÁNEK, Matej KLEMENT, Tadeáš DĚD, Jan ČERVENÝ a Luboš BRIM. Biochemical Space: A Language for Formal Description and Annotation of Complex Biological Processes. In Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2015.

BRIM, Luboš, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Coloured Model Checking Approach to Parameter Synthesis for Executable Models in Synthetic Biology. In Verification of Engineered Molecular Devices and Programs. 2015.

BRIM, Luboš, Juraj NIŽNAN a David ŠAFRÁNEK. Compact Representation of Photosynthesis Dynamics by Rule-based Models. Online. In 5th International Workshop on Static Analysis and Systems Biology (SASB 2014). 316. vyd. Neuveden: Elsevier, 2015, s. 17-27. ISSN 1571-0661. Dostupné z: https://dx.doi.org/10.1016/j.entcs.2015.06.008.

KLEMENT, Matej, David ŠAFRÁNEK, Jan ČERVENÝ, Tadeáš DĚD, Matej TROJÁK, Luboš BRIM a Stefan MUELLER. E-cyanobacterium.org: A Web-based Platform for Systems Biology of Cyanobacteria. In Fourth International Workshop on Hybrid Systems Biology. 2015.

BRIM, Luboš, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. High-Performance Discrete Bifurcation Analysis for Piecewise-Affine Dynamical Systems. In Alessandro Abate, David Šafránek. Hybrid Systems Biology Fourth International Workshop, HSB 2015, Madrid, Spain, September 4-5, 2015. Revised Selected Papers. LNCS 9271. Neuveden: Springer International Publishing, 2015, s. 58-74. ISBN 978-3-319-26915-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-26916-0_4.

BRIM, Luboš, Milan ČEŠKA, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Parameter Synthesis by Parallel Coloured CTL Model Checking. In Roux, Olivier and Bourdon, Jérémie. Computational Methods in Systems Biology. Neuveden: Springer International Publishing, 2015, s. 251-263. ISBN 978-3-319-23400-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-23401-4_21.

ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Model Checking C++ with Exceptions. Electronic Communications of the EASST. 2014, roč. 70, Listopad, s. 1-15. ISSN 1863-2122. Dostupné z: https://dx.doi.org/10.14279/tuj.eceasst.70.983.

ČEŠKA, Milan, David ŠAFRÁNEK, Sven DRAŽAN a Luboš BRIM. Robustness Analysis of Stochastic Biochemical Systems. Plos One. SAN FRANCISCO: PUBLIC LIBRARY SCIENCE, 2014, roč. 9, č. 4, s. 1-23. ISSN 1932-6203. Dostupné z: https://dx.doi.org/10.1371/journal.pone.0094553.

BRIM, Luboš, Petr DLUHOŠ, David ŠAFRÁNEK a Tomáš VEJPUSTEK. STL*: Extending signal temporal logic with signal-value freezing operator. Information and computation. Academic Press, 2014, roč. 236, January, s. 52-67. ISSN 0890-5401. Dostupné z: https://dx.doi.org/10.1016/j.ic.2014.01.012.

ROČKAI, Petr, Jiří BARNAT, Vladimír ŠTILL, Jiří WEISER, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK a Jan KRIHO. DIVINE 3.0. 2013.

BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO, Milan LENČO, Petr ROČKAI, Vladimír ŠTILL a Jiří WEISER. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Sharygina, Natasha; Veith, Helmut. Computer Aided Verification 2013. Heidelberg: Springer, 2013, s. 863-868. ISBN 978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8_60.

BRIM, Luboš, Milan ČEŠKA, Sven DRAŽAN a David ŠAFRÁNEK. Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. In 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Berlin: Springer Berlin Heidelberg, 2013, s. 107-123. ISBN 978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8_7.

ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. In Guillaume Brat, Neha Rungta, Arnaud Venet. NASA Formal Methods 2013. Neuveden: Springer, 2013, s. 1-15. ISBN 978-3-642-38087-7. Dostupné z: https://dx.doi.org/10.1007/978-3-642-38088-4_1.

BARNAT, Jiří, Luboš BRIM a Vojtěch HAVEL. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. In Juan E. Guerrero. Proceedings of Application of Concurrency to System Design, 2013. Barcelona: IEEE Computer Society, 2013, s. 51-59. ISBN 978-0-7695-5035-0. Dostupné z: https://dx.doi.org/10.1109/ACSD.2013.8.

BRIM, Luboš, Milan ČEŠKA a David ŠAFRÁNEK. Model Checking of Biological Systems. In Marco Bernardo. Formal Methods for Dynamical Systems. Neuveden: Springer, 2013, s. 63-112. ISBN 978-3-642-38873-6. Dostupné z: https://dx.doi.org/10.1007/978-3-642-38874-3_3.

BRIM, Luboš, Vilém DĚD a David ŠAFRÁNEK. Qualitative modelling and analysis of Photosystem II. Online. In CEUR Workshop Proceedings. Aachen: Neuveden, 2013, s. 17-29. ISSN 1613-0073.

BRIM, Luboš, Tomáš VEJPUSTEK, David ŠAFRÁNEK a Jana FABRIKOVÁ. Robustness Analysis for Value-Freezing Signal Temporal Logic. Online. In Proceedings HSB 2013. Neuveden: Neuveden, 2013, s. 20-36. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.125.

BRIM, Luboš, Milan ČEŠKA, Sven DRAŽAN a David ŠAFRÁNEK. Robustness Analysis of Stochastic Systems. Online. In Electronic Proceedings in Theoretical Computer Science, Volume 116. Turku: Open Publishing Association, 2013, s. 33-34. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.116.5.

VAN GOETHEM, Simon, Jean-Marie JACQUET, Luboš BRIM a David ŠAFRÁNEK. Timed Modelling of Gene Networks with Arbitrary Expression Level Discretization. Online. In Proceedings of the Third International Workshop on Interactions Between Computer Science and Biology (CS2Bio'12). Neuveden: Elsevier, 2013, s. 67-81. ISSN 1571-0661. Dostupné z: https://dx.doi.org/10.1016/j.entcs.2013.02.019.

BARNAT, Jiří, Petr BAUCH, Luboš BRIM a Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Journal of Parallel and Distributed Computing. Elsevier, 2012, roč. 72, č. 9, s. 1083-1097. ISSN 0743-7315. Dostupné z: https://dx.doi.org/10.1016/j.jpdc.2011.10.015.

BARNAT, Jiří, Luboš BRIM, Jan BERAN, Tomáš KRATOCHVÍLA a Italo Romani DE OLIVEIRA. Executing Model Checking Counterexamples in Simulink. In Tiziana Margaria, Zongyan Qiu, and Hongli Yang. IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering. Neuveden: IEEE Computer Society, 2012, s. 245-248. ISBN 978-0-7695-4751-0.

BARNAT, Jiří, Petr BAUCH a Luboš BRIM. Checking Sanity of Software Requirements. In George Eleftherakis , Mike Hinchey and Mike Holcombe. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. Thessaloniki: Springer, 2012, s. 48-62. ISBN 978-3-642-33825-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-33826-7_4.

BRIM, Luboš, Jana FABRIKOVÁ, Sven DRAŽAN a David ŠAFRÁNEK. On Approximative Reachability Analysis of Biochemical Dynamical Systems. In Corrado Priami et al. Transactions on Computational Systems Biology XIV. Heidelberg: Springer, 2012, s. 77-101. ISBN 978-3-642-35523-3. Dostupné z: https://dx.doi.org/10.1007/978-3-642-35524-0_4.

DLUHOŠ, Petr, Luboš BRIM a David ŠAFRÁNEK. On Expressing and Monitoring Oscillatory Dynamics. Electronic Proceedings in Theoretical Computer Science. Newcastle Upon Tyne: EPTCS, 2012, roč. 2012, č. 92, s. 73-87. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.92.

BARNAT, Jiří, Luboš BRIM, Adam KREJČÍ, Adam STRECK, David ŠAFRÁNEK, Martin VEJNÁR a Tomáš VEJPUSTEK. On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics. Los Alamitos: IEEE Computer Society, 2012, roč. 9, č. 3, s. 693-705. ISSN 1545-5963. Dostupné z: https://dx.doi.org/10.1109/TCBB.2011.110.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming. Elsevier, 2012, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2011.03.001.

BARNAT, Jiří, Jan BERAN, Luboš BRIM, Tomáš KRATOCHVÍLA a Petr ROČKAI. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical Systems (FMICS 2012). Berlin: Springer Berlin Heidelberg, 2012, s. 78--92. ISBN 978-3-642-32468-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-32469-7_6.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg, 2012, s. 252-266. ISBN 978-3-642-28890-6. Dostupné z: https://dx.doi.org/10.1007/978-3-642-28891-3_25.

BRIM, Luboš a Jakub CHALOUPKA. Using strategy improvement to stay alive. International Journal of Foundations of Computer Science. 2012, roč. 23, č. 3, s. 585-608. ISSN 0129-0541. Dostupné z: https://dx.doi.org/10.1142/S0129054112400291.

BARNAT, Jiří, Petr BAUCH, Luboš BRIM a Milan ČEŠKA. Computing Optimal Cycle Mean in Parallel on CUDA. Electronic Proceedings in Theoretical Computer Science. 2011, roč. 72, č. 2011, s. 68-83. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.72.8.

BARNAT, Jiří, Petr BAUCH, Luboš BRIM a Milan ČEŠKA. Computing Strongly Connected Components in Parallel on CUDA. In Proceedings of 25th IEEE International Parallel & Distributed Processing Symposium. Anchorage, AK: IEEE Computer Society, 2011, s. 544 - 555. ISBN 978-1-61284-372-8.

ŠAFRÁNEK, David, Jan ČERVENÝ, Matej KLEMENT, Jana POSPÍŠILOVÁ, Luboš BRIM, Dušan LAZÁR a Ladislav NEDBAL. E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes. BioSystems. Elsevier, 2011, roč. 103, č. 2, s. 115-124. ISSN 0303-2647. Dostupné z: https://dx.doi.org/10.1016/j.biosystems.2010.10.013.

BRIM, Luboš, Jakub CHALOUPKA, Laurent DOYEN, Raffaella GENTILINI a Jean-François RASKIN. Faster algorithms for mean-payoff games. Formal Methods in System Design. Springer Netherlands, 2011, roč. 38, č. 2, s. 97-118. ISSN 0925-9856. Dostupné z: https://dx.doi.org/10.1007/s10703-010-0105-x.

EDELKAMP, Stefan, Damian SULEWSKI, Jiří BARNAT, Luboš BRIM a Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Science of Computer Programming. Elsevier, 2011, roč. 76, č. 2, s. 136--157. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2010.03.005.

BENEŠ, Nikola, Luboš BRIM, Barbora BÜHNOVÁ, Ivana ČERNÁ, Jiří SOCHOR a Pavlína MORAVCOVÁ VAŘEKOVÁ. Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata. Science of Computer Programming. Elsevier, 2011, roč. 76, č. 10, s. 877-890. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2010.02.008.

BRIM, Luboš a Jiří BARNAT. Platform Dependent Verification: On Engineering Verification Tools for 21st Century. Electronic Proceedings in Theoretical Computer Science. 2011, roč. 72, č. 2011, s. 1-12. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.72.1.

BRIM, Luboš, Jana FABRIKOVÁ, Sven DRAŽAN a David ŠAFRÁNEK. Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. Electronic Proceedings in Theoretical Computer Science. 2011, Neuveden, č. 67, s. 97-112, 15 s. ISSN 2075-2180. Dostupné z: https://dx.doi.org/10.4204/EPTCS.67.9.

BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA a Petr ROČKAI. DiVinE: Parallel Distributed Model Checker (Tool paper). In Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010). 2010, 4 s.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE 2.4. 2010.

BARNAT, Jiří, Petr BAUCH, Luboš BRIM a Milan ČEŠKA. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010). Neuveden: IEEE Computer Society, 2010, s. 259-266. ISBN 978-0-7695-4307-9.

KLEMENT, Matej, David ŠAFRÁNEK, Jan ČERVENÝ, Luboš BRIM a Ladislav NEDBAL. E-photosynthesis: web software for modeling and analysis of biological processes behind photosynthesis. 2010.

BARNAT, Jiří, Luboš BRIM a David ŠAFRÁNEK. High-performance analysis of biological systems dynamics with the DiVinE model checker. Briefings in Bioinformatics. Oxford (UK): Oxford University Press, 2010, roč. 11, č. 3, s. 301-312. ISSN 1467-5463.

BARNAT, Jiří, Luboš BRIM, Petr BAUCH a Milan ČEŠKA. MWC-DiVinE. 2010.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010, s. 222-231. ISBN 978-0-7695-4153-2.

BARNAT, Jiří, Luboš BRIM, David ŠAFRÁNEK a Martin VEJNÁR. Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. In Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology. Los Alamitos: IEEE Computer Society, 2010, s. 95-104. ISBN 978-0-7695-4265-2.

APPL, Jiří, Jiří BARNAT, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE 2.0. 2010.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, roč. 12, č. 2, s. 139-153. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-010-0136-z.

BRIM, Luboš a Jakub CHALOUPKA. Using Strategy Improvement to Stay Alive. In Games, Automata, Logics and Formal Verification (GandALF) 2010. Neuveden: Electronic Proceedings in Theoretical Computer Science (EPTCS), 2010, s. 40-54. ISSN 2075-2180.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany: Springer Berlin / Heidelberg, 2009, s. 407-425. ISBN 978-3-642-10372-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-10373-5_21.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ, Jan LÁNÍK, David ŠAFRÁNEK a Ma HONGWU. BioDiVinE: A Framework for Parallel Analysis of Biological Models. In Proceedings of 2nd International Workshop on Computational Models for Cell Processes. Neuveden: EPTCS, 2009, s. 31-45. ISSN 2075-2180.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ, Jan LÁNÍK a David ŠAFRÁNEK. BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. In Computational Mehotds in Systems Biology: Abstract of the Posters. Pisa: University of Pisa, 2009, s. 1-5, 4 s.

BARNAT, Jiří, Luboš BRIM, Stefan EDELKAMP, Damian SULEWSKI a Pavel ŠIMEČEK. Can Flash Memory Help in Model Checking? In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, s. 150-165. ISBN 978-3-642-03239-4. Dostupné z: https://dx.doi.org/10.1007/978-3-642-03240-0_14.

BARNAT, Jiří, Luboš BRIM a Pavel ŠIMEČEK. Cluster-Based I/O-Efficient LTL Model Checking. In 24th IEEE/ACM International Conference on Automated Software Engineering. Los Calamitos (California): IEEE Computer Society, 2009, s. 635-639. ISBN 978-0-7695-3891-4.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ a David ŠAFRÁNEK. Computational Analysis of Large-Scale Multi-Affine ODE Models. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009, s. 81-90. ISBN 978-0-7695-3809-9.

BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA a Tomáš LAMR. CUDA Accelerated LTL Model Checking. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden: Roy Sterritt, 2009, s. 34-41. ISBN 978-0-7695-3900-3.

BARNAT, Jiří, Luboš BRIM, Petr BAUCH, Milan ČEŠKA a Tomáš LAMR. DiVinE Cuda. 2009.

ROČKAI, Petr, Jiří BARNAT, Luboš BRIM a Milan ČEŠKA. DiVinE 2.0. 2009.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE 2.0: High-Performance Model Checking. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009, s. 31-32. ISBN 978-0-7695-3809-9.

BARNAT, Jiří, Luboš BRIM a Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science. 2009, roč. 14, Prosinec, s. 107--111. ISSN 2075-2180.

VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT a Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009, s. 201-212. ISBN 978-1-4244-3751-1.

CHALOUPKA, Jakub a Luboš BRIM. Faster Algorithm for Mean-Payoff Games. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Dagstuhl, Německo: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo, 2009, 9 s. ISBN 978-3-939897-15-6.

CHALOUPKA, Jakub a Luboš BRIM. Faster Algorithm for Mean-Payoff Games. In MEMICS 2009. Brno: NOVPRESS s.r.o., 2009, s. 45-53. ISBN 978-80-87342-04-6.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, s. 53-68. ISBN 978-3-642-03239-4. Dostupné z: https://dx.doi.org/10.1007/978-3-642-03240-0_8.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ a David ŠAFRÁNEK. On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science. 2009, roč. 2009, č. 410, s. 3128-3148, 20 s. ISSN 0304-3975.

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. Partial Order Reduction for State/Event LTL. In Proceedings of the International Conference on Integrated Formal Methods (IFM'09). Berlin / Heidelberg, Germany: Springer Verlag, 2009, s. 307-321. ISBN 978-3-642-00254-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-00255-7_21.

BARNAT, Jiří, Luboš BRIM, Stefan EDELKAMP, Damian SULEWSKI a Pavel ŠIMEČEK. Can Flash Memory Help in Model Checking? In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla: ERCIM, 2008, s. 159-174.

ZIMMEROVÁ, Barbora, Pavlína VAŘEKOVÁ, Nikola BENEŠ, Ivana ČERNÁ, Luboš BRIM a Jiří SOCHOR. Component-Interaction Automata Approach (CoIn). In The Common Component Modeling Example: Comparing Software Component Models. Berlin / Heidelberg, Germany: Springer Verlag, 2008, s. 146-176. LNCS 5153. ISBN 978-3-540-85288-9.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Pavel ŠIMEČEK. DiVinE Cluster. 2008.

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Á, Sven DRAŽAN a David ŠAFRÁNEK. From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks. In Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation. Budapest: Ivana Cerna and Gerald Luettgen, 2008, s. 83-96, 15 s. ISSN 1571-0661.

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Á, Sven DRAŽAN a David ŠAFRÁNEK. Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. In Electronic Notes in Theoretical Computer Science. Vol. 194/3. Elsevier: Elsevier Science, 2008, s. 35-50, 15 s. ISSN 1571-0661.

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. Partial Order Reduction for State/Event LTL. Brno, Czech Republic: Faculty of Informatics, Masaryk University, 2008, 21 s. Technical report FIMU-RS-2008-07.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE-MC. 2008.

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ří, Luboš BRIM, Pavel ŠIMEČEK a Michael WEBER. Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2008, s. 48-62. ISBN 978-3-540-78799-0.

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.

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08). Málaga, Spain: Department of Computer Science, University of Málaga, 2008, s. 221-225. ISSN 1571-0661.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core. 2007.

BARNAT, Jiří, Luboš BRIM a Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007, s. 281-293. ISBN 978-3-540-73367-6.

BRIM, Luboš a Mojmír KŘETÍNSKÝ. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2007, s. 9-28. ISBN 978-3-540-69506-6.

BARNAT, Jiri, Lubos BRIM a Martin LEUCKER. Parallel Model Checking and the FMICS-jETI Platform. In Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems. Los Alamitos: IEEE Computer Society, 2007, s. 330-339. ISBN 0-7695-2895-3.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE. 2007.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE: A Parallel Qualitative LTL Model Checker. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07). United States of America: IEEE Computer Society, 2007, s. 215-216. ISBN 0-7695-2883-X.

BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1. vyd. Berlin, Heidelberg: Springer-Verlag, 2007, s. 187-203. ISBN 978-3-540-73369-0.

BRIM, Luboš a Jiří BARNAT. Tutorial: Parallel Model Checking. In Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2007, s. 2-3. ISBN 978-3-540-73369-0.

BARNAT, Jiří, Luboš BRIM a Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006, s. 259-279. ISBN 978-3-540-36749-9.

BRIM, Luboš, Ivana ČERNÁ, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. Software engineering notes : an informal newsletter of the Special Interest Committee on Software Engineering. [New York, N.Y.?]: ACM, 2006, roč. 31, č. 2, s. 1-8. ISSN 0163-5948.

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š. Distributed Verification: Exploring the Power of Raw Computing Power. In 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006). Bonn, Germany: TU Munchen, 2006, s. 23-34, 15 s. ISBN 3-540-70951-7.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Pavel MORAVEC, Petr ROČKAI a Pavel ŠIMEČEK. DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin: Springer Verlag, 2006, s. 278-281. ISBN 978-3-540-37406-0.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Pavel MORAVEC, Pavel ŠIMEČEK a Jakub CHALOUPKA. DiVinE Library. 2006.

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.

BRIM, Luboš a Isabelle LINDEN. Proceedings of the First International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2005). NIzozemsko: Elsevier, 2006, 159 s. ENTCS Volume 150, Issue 1. ISBN 1571-0661.

BRIM, Luboš a Martin LEUCKER. Special Issue on Parallel and Distributed Verification - Foreword. Formal Methods in System Design. Springer Netherlands, 2006, roč. 29, č. 2, s. 115-116. ISSN 0925-9856.

BRIM, Luboš. Účast ČR ve výzkumném sdružení ERCIM. 2006.

BRIM, Luboš a Martin LEUCKER. 11th International Workshop on Formal Methods for Industrial Critical Systems. 2006.

BRIM, Luboš, Jitka ŽIDKOVÁ a Karen YORAV. Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, roč. 7, č. 1, s. 61-73, 14 s. ISSN 1433-2779.

BRIM, Luboš, Ivana ČERNÁ, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. In Proceedings of SAVCBS 2005. Ames, USA: Department of Computer Science, Iowa State University, 2005, s. 31-38.

BARNAT, Jiří, Luboš BRIM a Ivana ČERNÁ. Distributed Analysis of Large Systems. In Formal Methods for Components and Objects. Amsterdam: CWI Amsterdam, 2005, s. 31-35, 4 s.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Distributed Partial Order Reduction of State Spaces. Electronic Notes on Theoretical Computer Science. Elsevier, 2005, roč. 128, č. 3, s. 63-74. ISSN 1571-0661.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ a Pavel ŠIMEČEK. DIVINE - The Distributed Verification Environment. In In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisboa, Portugal: TU Munchen, 2005, s. 89-94.

PELÁNEK, Radek, Tomáš HANŽL, Ivana ČERNÁ a Luboš BRIM. Enhancing Random Walk State Space Exploration. In Formal Methods for Industrial Critical Systems. Lisbon: ACM SIGSOFT, 2005, s. 98-105. ISBN 1-59593-148-1.

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.

BRIM, Luboš a Orna GRUMBERG. Introductory paper: Parallel and Distributed Model Checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, roč. 7, č. 1, s. 1-3. ISSN 1433-2779.

BRIM, Luboš a Isabelle LINDEN. MTCoord 2005 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems. 2005.

BRIM, Luboš a Isabelle LINDEN. Proceedings of the 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems. Namur, Belgie: FNDP Namur, 2005, 105 s. Tech. Rep.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Under-Approximation Generation using Partial Order Reduction. Brno: Faculty of Informatics, 2005, 21 s. Technical Reports, FIMU-RS-2005-04.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. Brno: Faculty of Informatics, 2004, 22 s. Technical Reports, FIMU-RS-2004-09.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD). Neuveden: Springer-Verlag, LNCS 3312, 2004, s. 352-366, 24 s. ISBN 3-540-23738-0.

BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. Distributed Memory LTL Model Checking Based on Breadth First Search. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 s. FIMU-RS-2004-07.

BRIM, Luboš, Ivana ČERNÁ a Lukáš HEJTMÁNEK. Distributed Negative Cycle Detection Algorithms. In Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Nizozemsko: Elsevier B.V., 2004, s. 297-305. ISBN 0-444-51689-1.

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Distributed Partial Order Reduction of State Spaces. In Proceedings of the 3rd International Workshop on Parallel and Distributed Verifationic (PDMC 2004). London, U.K.: Imperial College London, 2004, s. 3-18, 15 s.

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.

BRIM, Luboš. Parallel Model-Checking. ERCIM News. ERCIM EEIG, 2004, roč. 58, June, s. 35-36. ISSN 0926-4981.

BRIM, Luboš, Jean-Marie JACQUET, David GILBERT a Mojmír KŘETÍNSKÝ. Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. Electronic Notes in Theoretical Computer Science. Amsterdam: Elsevier Science, 2003, roč. 68, č. 3, s. 1-24. ISSN 0444514163.

BRIM, Luboš a Jiří BARNAT. Distribution of Explicit-State LTL Model-Checking. Editors Thomas Arts, Wan Fokking. Electronic Notes in Theoretical Computer Science. Elsevier Science, 2003, Volume 80, č. 1, s. 120-125.

BRIM, Luboš, Jean-Marie JACQUET, David GILBERT a Mojmír KŘETÍNSKÝ. Modelling Multi-Agents Systems as Concurrent Constraint Processes. Computing and Informatics. 2003, roč. 21, č. 6, s. 565-590, 25 s. ISSN 1335-9150.

BRIM, Lubos, Ivana ČERNÁ a Lukáš HEJTMÁNEK. Parallel Algorithms for Detection of Negative Cycles. In Proceedings of the 10th ParCo Conference. Holandsko: Elsevier B.V., 2003, s. 98-111.

BRIM, Lubos, Ivana ČERNÁ a Lukáš HEJTMÁNEK. Parallel Algorithms for Detection of Negative Cycles. Brno: Faculty of Informatics, 2003, 14 s. Technical Reports, FIMU-RS-2003-04.

BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03). Montreal: IEEE Computer Society, 2003, s. 106-115. ISBN 0-7695-2035-9.

BRIM, Luboš a Orna GRUMBERG. PDMC 2003 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2003, 130 s. ENTCS, Vol. 89, No. 1.

BRIM, Luboš a Jitka ŽÍDKOVÁ. Using Assumptions to Distribute Alternation Free mu-Calculus Model Checking. In 2st International Workshop on Parallel and Distributed Model Checking (PDMC 2003). Boulder, Colorado, USA. Brno, Czech Republic: Elsevier, 2003, s. 19-34.

BRIM, Luboš. Automatizovaná formální verifikace. In XXI. conference EurOpen 2002. Znojmo, Czech republic. Znojmo, Czech Republic: EuroOpen.cz, Praha, 2002, s. 1-7. ISBN 80-86583-00-7.

BRIM, Luboš, Petr JANČAR, Mojmír KŘETÍNSKÝ a Antonín KUČERA. CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings. Berlin, Heidelberg, New York: Springer, 2002, 609 s. Lecture Notes in Computer Science, vol. 2421. ISBN 3-540-44043-7.

BRIM, Luboš, Jean-Marie JACQUET, David GILBERT a Mojmír KŘETÍNSKÝ. Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. In Foundations of Coordination Languages and Software Architecture (FOCLASA`02). Amsterdam: Namur University, 2002, s. 1-24.

BRIM, Luboš a Orna GRUMBERG. PDMC 2002 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2002, 165 s. ENTCS, Vol. 68, No. 4. ISBN 0444512918.

BARNAT, Jiří, Luboš BRIM a Ivana ČERNÁ. Property Driven Distribution of Nested DFS. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic. Pittsburgh, PA, USA: Dept. of Electronics and Computer Science, University of Southampton, 2002, s. 1-10.

BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV. Using Assumptions to Distribute CTL Model Checking. In 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002). Brno, Czech Republic: Elsevier, 2002, s. 80-95. ISBN 0444512918.

BRIM, Luboš, Jitka CRHOVÁ a Karen YORAV. Using Assumptions to Distribute CTL Model Checking. Brno, Czech Republic, 2002, s. 1-22. Technical Report FIMU-RS-2002-08.

BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK. Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India: Springer, 2001, s. 96-110. LNCS 2245. ISBN 3-540-43002-4.

BARNAT, Jiří, Luboš BRIM a Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. In M.B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop. Toronto, Canada: Springer Verlag, 2001, s. 200-215. ISBN 3-540-42124-6.

BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK. How to Employ Reverse Search in Distributed Single-Source Shortest Paths. How to Employ Reverse Search in Distributed Single-Source Shortest Paths. In SOFSEM 2001. Piestany: Springer, 2001, s. 191-200. LNCS 2234. ISBN 3-540-42912-3.

BRIM, Luboš, Jean-Marie JACQUET, David GILBERT a Mojmír KŘETÍNSKÝ. Multi-Agents Systems as Concurrent Constraint Processes. In SOFSEM 2001 28th Conf.on Current Trends in Theory and Practice of Informatics. Heldelberg: Springer Verlag, 2001, s. 201-210. Lecture Notes in Computer Science, vol.2234. ISBN 0302-9743.

BRIM, Luboš, Ivana ČERNÁ a Martin NEČESAL. Randomization Helps in LTL Model Checking. In Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001. Berlin Heidelberg New York: Springer, 2001, s. 105-119. LNCS 2165. ISBN 3-540-42556-X.

BARNAT, Jiří, Luboš BRIM a Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. Brno: FI MU, 2000, 16 s. Technical Reports.

BRIM, Luboš, Jean-Marie JACQUET, David GILBERT a Mojmír KŘETÍNSKÝ. A Fully Abstract Semantics for a Version of Synchronous Concurrent Constraint Programming. FI MU Report Series. Brno: FI MU, 1999, roč. 1999, č. 08, s. 1-62.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A fully abstract semantics for synchronous and asynchronous ccp. Technical Report of Namur University. Namur: Namur University, 1998, roč. 1998, č. 1, s. 1-48.

BRIM, Luboš, Jozef GRUSKA a Jiří ZLATUŠKA. Mathematical Foundations of Computer Science 1998. Heidelberg: Springer Verlag, 1998, 846 s. Lecture Notes in Computer Science, Vol. 1450. ISBN 3-540-64827-5.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Adding Time via Timed Transitions to Concurrent Constraint Programming. In ERCIM/COMPULOG Workshop. Linz, Austria: ERCIM, 1997, s. 23-34.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Temporal Synchronous Concurrent Constraint Programming. In COTIC 97, 1st Int.Workshop on Contr.programming for time critical systems. Piza, Italy: COTIC 97, 1997, s. 35-50. tical appl.

BRIM, Lubos, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A process algebra for Synchronous Concurrent Constraint Programming. In ALP96: Fifth Int. Conference on Algebraic and Logic Programm. Aachen, Germany: Springer-Verlag, 1996, s. 165-178. LNCS 1139. ISBN 3-540-61735-3.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A process Algebra for Synchronous Concurrent Constraint Programming. TR City University, U.K. London: City University London, 1996, roč. 1996, č. 6, s. 1-15. ISSN 1364-4009.

BRIM, Lubos, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. New versions of asks for synchronous communication in concurrent constraint programming. TR City University, U.K. London: City University London, 1996, roč. 1996, č. 3, s. 1-22. ISSN 1364-4009.

BRIM, Lubos, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A process algebra for Synchronous Concurrent Constraint Programming. Technical Report of Namur University. Namur: Namur University, 1995, roč. 1995, č. 8, s. 1-15.

BRIM, Lubos, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. New versions of Ask and Tell for synchronous communication in CCP. TR City University, U.K. London: City University London, 1995, roč. 1995, č. 10, s. 1-18. ISSN 1364-4009.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Synchronisation in Scc. In ILPS´95. Portland, Oregon, U.S.A: MIT Press, 1995, s. 282-283. ISBN 0-262-62099-5.

BRIM, Luboš. Modal mu-Calculus with Distances. Scripta Fac.Brun. 1994, roč. 1994, č. 23, s. 51-63. ISSN 2101-2986.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. On Synchronous Communication in Concurrent Constraint Programming. Technical Report of Namur University. Namur: Namur University, 1994, roč. 1994, prelim.rep, s. 1-25.

BRIM, Luboš, David GILBERT, Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Operational semantics of concurrent logical systems. In ALP-UK Workshop on Cocurrency in Computational Logic. London,U.K.: City University London, 1993, s. 13-18.

BRIM, Luboš. Analysing time aspects of dynamic systems. In Proc. EMCSR'92. World Scientific, 1992, s. 1024-1035. ISBN 981-02-1991-1.

BRIM, Luboš. Modal logics for timed process algebras. In First North American First North American Process Algebra Workshop. Workshops in Computing, Springer-Verlag, 1992, s. 13-28. ISBN 3-540-19822-9.

BRIM, Luboš a Jiří HOŘEJŠ. DIJKSTROVŠTINY aneb programování jako věda. In Proc. SOFSEM 84. 1984, s. 39-68.

HOŘEJŠ, Jiří a Luboš BRIM. Automatická syntéza programů. In Proc. SOFSEM 82. 1982, s. 277-308.