prof. RNDr. Luboš Brim, CSc.

Curriculum vitae

Person Identification

• Prof. RNDr. Luboš Brim, CSc.

Workplace

• Department of Computer Science, Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00 Brno, Czech Republic

Employment Position

• Professor

Education and Academic Qualifications

• 2006: Professor in Informatics, Masaryk University, Brno;
• 1996: Associate Professor (Docent) in Computer Science, Faculty of Informatics, Masaryk University Brno; habilitation thesis: Modal Logics for Real-Time Systems
• 1986: PhD (CSc.) in Theoretical Computer Science, Czechoslovak Academy of Science; thesis: Structural Specifications of Predicate Transformers
• 1979: RNDr. (M.Sc. by research) in Computer Science, Faculty of Sciences, Masaryk University Brno; thesis: Propositional Dynamic Logic
• 1976: graduated in Mathematics (with honors), Faculty of Sciences, University of Brno; thesis: Proving Program Correctness

Employment Summary

• 2004 - 2011: Vice-Dean for International Studies, First Vice-Dean, Faculty of Informatics, MU Brno
• 1994 - 2017: Vice-Head of the Department of Computing Science, MU Brno
• 1998 - 2000: Vice-Dean for Research, Faculty of Informatics, MU Brno
• 2006 - now: Professor of Informatics, Masaryk University, Brno
• 1996 - 2006: Associate Professor of Computer Science, Masaryk University Brno
• 1976 - 1996: Assistant Professor of Computer Science, Masaryk University Brno
• 1976 - 1980 Assistant Professor of Computer Science, Technical University Brno

Pedagogical Activities

• Logic and Programming, Software Engineering, Modal and Temporal Logics, Computability and Complexity, Communication and Parallelism, Program Verification, Computational Systems Biology.
  Projects:
• 1992-1994: Trans-European Mobility Scheme for University Studies (TEMPUS) program, JEP 2891, "Technology Transfer in Information technologies", (project leader at FI)
• 2009-2012: Innovation of bachelor and master degree programes in the direction to systems biology (ESF)
  Past doctoral students:
• Jitka Žídková. Using Assumptions to Distribute Model Checking. 2004
• Jiří Barnat. Distributed Memory LTL Model Checking. 2005
• David Šafránek. Visual Coordination Networks. 2006
• Pavel Moravec. Distributed State Space Reductions. 2008
• Pavel Šimeček. External Memory LTL Model Checking. 2010
• Jakub Chaloupka. Algorithms for Mean-Payoff and Energy Games. 2011
• Milan Češka. Designing Data-Parallel Graph Algorithms for Model Checking. 2012
• Martin Demko. Model Checking Based Parameter Synthesis of Dynamical Systems in Biology. 2019
• Samuel Pastva. Digital Bifurcation Analysis: On the Qualities of Long-term Behaviour in Discrete Systems. 2022
• Jana Dražanová.Abstraction-Based Analysis of Continuous-Time Models in System Biology. 2022
• Matej Troják. Rule-Based Modelling of Biochemical Processes: Specification and Analysis. 2023

Scientific and Research Activities

• Research Interests:
  Formal verification, modal and temporal logics, time-critical systems, formal methods, verification tools, analysis of embedded and component-based systems, modeling and parameter estimation in systems biology.
  Projects:
• 2018 - 2020: Czech Science Foundation: Discrete Bifurcation Analysis of Reactive Systems (project leader)
• 2015 - 2017: Czech Science Foundation: Parameter Discovery for Biological Models Using Model Checking (project leader)
• 2010 - 2013: Artemis Joint Undertaking: "CRYSTAL - Critical System Engineering Acceleration" (co-worker)
• 2011 - 2013: Czech Science Foundation: Software Components in Embedded Systems: Development and Verification (co-worker)
• 2010 - 2013: Artemis Joint Undertaking: "iFEST - industrial Framework for Embedded Systems Tools" (site leader)
• 2009 - 2011: Czech Science Foundation: "Verification and Analysis of Large-Scale Computer Systems" (project leader)
• 2007 - 2009: FP6 STREP: EC-MOAN - Scalable Modeling and Analysis Techniques to Study Emergent Cell Behavior (site leader)
• 2004 - 2008: FP6 NoE: ARTIST2 Network of Excellence on Embedded Systems Design (affiliated academic partner, site leader)
• 2005 - 2009: Academy of Sciences of Czech Republic: Techniques for automatic verification and validation of software and hardware systems (project leader)
• 2003 - 2005: Grant Agency of Czech Republic: "Automated Verification of Parallel and Distributed Systems", grant no. 201/03/0509 (project leader)
• 2000 - 2002: Grant Agency of Czech Republic: "Algorithms and Tools for Practical Verification of Concurrent Systems", grant no. 201/00/1023 (project leader)
• 2000 - 2002: Grant Agency of Czech Republic: "Infinite State Concurrent Systems -- Models and Verification", grant no. 201/00/0400 (co-worker)
• 1999 - 2003: Research Intent of Faculty of Informatics, MU: "Models of Nonsequentinal Computing", grant no.: CEZ: J07/98: 143300001 (co-worker, project leader: J. Gruska)
• 1997 - 1999: Grant Agency of Czech Republic: "Algorithmic verification boundaries for infinite state systems", grant no. 201/97/0456(co-worker)
• 1996: Royal Academy, U.K.: "Temporal and distributed concurrent constraint systems" (project leader)
• 1993 - 1996: EU COST 247.01 "Verification and validation methods for formal description" (co-worker)
• 1993 - 1995: Grant Agency of Czech Republic "Analysis of concurrent infinite state systems", grant number 201/93/2123 (co-worker)
• 1993: European Community's Action for Cooperation in Science and Technology with Central and Eastern European Countries; "Specification and Analysis of Real-Time Systems"
• Grants of SPZV ČSAV ("Program Correctness", 1980 -- 1985 (co-worker); "Modern Programming Methodologies", 1986 -- 1990 (project leader))
  Publications summary: 2 books, over 50 journal and conference papers, and research reports, over 60 reviews in professional review journals (Journal of Logic and Computation, Journal of the IGPL, Computers and Artificial Inteligence, Information Systems, and Zentralblatt fur Mathematik)

Academical and Research Stays

• 1984 - Institute of Technology, Dresden, Germany, 1 month
• 1989 - Oxford University Computing Laboratory, PRG, Oxford, UK, 3 months
• 1992 - Staffordshire Polytechnic, School of Computing, Stafford, UK, 4 months
• 1993 - Dublin Institute of Technology, Ireland, 1 month
• 1993 - Imperial College, London, UK, 2 weeks
• 1993 - City University, London, UK, 3 months
• 1994 - Imperial College, London, UK, 2 weeks
• 1995 - Aarhus University, Aarhus, Denmark, 2 weeks
• 1996 - City University, London, UK, 2 months
• 1997 - City University, London, UK, 3 weeks
• 1997 - 2004 - short-term visits to City University, London, UK and Namur University, Belgium

University Activities

• 2004 - 2017: member of Scientific Council, Faculty of Informatics, Masaryk University
• 1998 - 2000: member of Scientific Council, Faculty of Informatics, Masaryk University
• 1998 - 2017: member of Advisory Board for PhD studies in Computer Science (Faculty of Informatics, Masaryk University)

Extrauniversity Activities

• 2003 - 2017: member of Advisory Board for PhD studies in Information Technology, Faculty of Information Technology, Technical University Brno
• 1999 - 2008: member of the ERCIM executive committee
• 1999 - 2008: executive director of CRCIM
• 1998 - 2002: member of Scientific Council, Faculty of Electrical Engineering and Infromatic, Technical University Brno
• 1998 - 2006: member of the Czech Acreditation Committee for Informatics and Mathematics
• 1996 - 1999: Honorary Research Fellow, City University, London, UK.
  Membership in Professional Societies: European Association for Theoretical Computer Science(EATCS), ERCIM working group on FMICS, ERCIM Working Group on Constraints, Interest Group for Propositional Logic (IGPL), Czech Society for Informatics

Appreciation of Science Community

• Committee member of international conferences and workshops:
  CONCUR (2002 general conference chair)
  PDMC (2002 co-chair, 2003 co-chair, 2004 co-chair, 2005, 2009 co-chair, 2010, 2011,2012)
  SOFSEM (2000,2002 - Students research Forum)
  FMICS (2003, 2004, 2005, 2006 co-chair, 2007, 2008, 2009, 2010,2012)
  FME (2003)
  HiBi (2009, 2010)
  MTCoord (2005 co-chair, 2006, 2007, 2008)
  SPIN (2008, 2009)
  FORMATS (2011)
  TIME (2011)
  Compmod (2009,2011, 2013)
  TASE (2012,2013,2015)
  TIP (2012,2013)
  TACAS (2018)
• member of FMICS and PDMC steering committees
• Dagstuhl 2008: Distributed Verification and Grid Computing
• Dagstuhl 2009: Graph Search Engineering

Selected Publications

• 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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• BRIM, Luboš, Samuel PASTVA, David ŠAFRÁNEK a Eva ŠMIJÁKOVÁ. Parallel One-Step Control of Parametrised Boolean Networks. Mathematics. Switzerland: MDPI, 2021, roč. 9, č. 5, s. 1-16. ISSN 2227-7390. Dostupné z: https://dx.doi.org/10.3390/math9050560. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• Š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. URL info
• 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. URL info
• 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. URL info
• 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. info
• Š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. info
• 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. URL info
• Č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. URL info
• 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. URL info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. info
• 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. URL info
• 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. info
• 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. info
• 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. info
• Č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. info
• 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. info
• 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. URL info
• 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. info
• 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. elektronická verze v nakladatelství Springer info
• 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. info
• 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. URL info
• 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. URL info
• 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. info
• Č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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. info
• 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. URL info
• ŠAFRÁNEK, David, Jan ČERVENÝ, Matej KLEMENT, Luboš BRIM, Dušan LAZÁR a Ladislav NEDBAL. E-photosynthesis.org: Web-based platform for photosynthetic processes. In 10th International Conference on Computational Methods in Systems Biology (CMSB 2012). 2012. Programme of CMSB 2012 incl. list of posters Regular poster presented at CMSB 2012 info
• 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. URL info
• Š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. URL info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. EPTCS info
• 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. EPTCS volume 72 info
• 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. info
• 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. DOI Abstract PDF reprint info
• 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. URL info
• 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. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. URL info
• 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. info
• 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. info
• BARNAT, Jiří, Sven DRAŽAN, Jana FABRIKOVÁ, David ŠAFRÁNEK, Luboš BRIM, Ivana ČERNÁ a Jan LÁNÍK. BioDiVinE. 2009. URL info
• 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. URL info
• 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. info
• 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. URL info
• 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. info
• 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. info
• 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. info
• BARNAT, Jiří, Luboš BRIM, Petr BAUCH, Milan ČEŠKA a Tomáš LAMR. DiVinE Cuda. 2009. URL info
• ROČKAI, Petr, Jiří BARNAT, Luboš BRIM a Milan ČEŠKA. DiVinE 2.0. 2009. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN a David ŠAFRÁNEK. Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. In Preproceedings of the Workshop From Biology to Concurrency and Back. Lisbon: Complex System Research Group, University of Camerino, 2007, s. 80-95, 15 s. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• BRIM, Luboš a Martin LEUCKER. 11th International Workshop on Formal Methods for Industrial Critical Systems. 2006. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. URL info
• BRIM, Luboš a Isabelle LINDEN. MTCoord 2005 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems. 2005. info
• 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. info
• BRIM, Luboš. Parallel Model-Checking. ERCIM News. ERCIM EEIG, 2004, roč. 58, June, s. 35-36. ISSN 0926-4981. URL info
• 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. info
• 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. info
• 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. URL info
• 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. info
• 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. info
• 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. URL info
• 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. URL info
• 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. URL info
• 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. info
• 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. info
• BRIM, Luboš a Orna GRUMBERG. PDMC 2003 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2003, 130 s. ENTCS, Vol. 89, No. 1. info
• 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. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK. Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths. Brno: FI MU, 2001, 19 s. Technical Reports, FIMU-RS-2001-01. URL info
• BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL a Radek PELÁNEK. How to Employ Reverse Search in Distributed Single-Source Shortest Paths. Brno: FI MU, 2001, 22 s. Technical Reports, FIMU-RS-2001-09. URL info
• 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. URL info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• BRIM, Luboš. Modal logics for real-time systems. Brno, 1995, 107 s. info
• BRIM, Luboš. Modal mu-Calculus with Distances. Scripta Fac.Brun. 1994, roč. 1994, č. 23, s. 51-63. ISSN 2101-2986. info
• 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. info
• BRIM, Luboš. Analysing time aspects of dynamic systems. In Proc. EMCSR'92. World Scientific, 1992, s. 1024-1035. ISBN 981-02-1991-1. info
• 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. info

2023/12/20