I am a professor at the Department of Computer Science, Faculty of Informatics, Masaryk University.
I have an M.S. in Mathematics from Masaryk University (1976) and a PhD in Computer Sciences from the Czech Academy of Sciences (1986) under Professor J. Horejs. Since 2006 I am a full professor of informatics at Masaryk University.
My current research interests include automated formal verification, parallel verification and digital systems biology.
In 2009, I founded the Laboratory of Systems Biology intending to integrate and intensify research and education activities in the emerging area of Computational Systems Biology at the Faculty of Informatics, Masaryk University.
From January 1, 2016, we became part of the national research infrastructure C4Sys (Centre for System Biology), representing a Czech node of the ISBE (Infrastructure for Systems Biology – Europe), and our activities are supported from the program for large research infrastructures of the Ministry of Education, Youth and Sports.
For a more detailed CV, please follow this external link and check My Academic Genealogy.
The aim of our research in digital systems biology is to enhance our understanding of the molecular mechanisms underlying the behaviour of complex living systems. The goal is to gain a better explanation of how the complex dynamic behaviour of the cell emerges from the interactions of molecular species. When solving such a non-trivial goal, the data have to be necessarily integrated with mathematical modelling and computer analysis. Since the complexity of biological networks is enormous due to the appearance of complicated feedback loops, the system dynamics is often counter-intuitive and cannot be directly predicted from the network structure.
Computer science technologies together with computer tools employing suitable mathematical and computer science methods can help to obtain an exact description of the networks, and in consequence, to infer interesting predictions of systems dynamics evolved in an arbitrary environment. To cope with large-scale biological models describing interaction in the scale of several functional layers of a living cell, the central requirement imposed on analysis tools is the scalability.
My current primary research topic focus
Boolean network is a very simple model of a biological system: each node takes either 0 or 1 and the states of nodes change according to regulation rules given as Boolean functions. In partially specified Boolean networks, some of these Boolean functions are (partially) unknown. Viewed in another way, we only know values of the Boolean functions for some arguments. The goal of our research is to develop effective, fast, and scalable methods, techniques and tools for automated analysis of robustness and control of partially defined Boolean networks.
I don't have an office phone and my university number is inactive.
surname at fi.muni.cz
Faculty of Informatics
Botanicka 68a
602 00 BRNO
Czech Republic
Room A411
Wednesday 9.00-10.00
or by appointment
Každý program je zpravidla strukturován do několika dílčích menších programů, které realizují část z požadovaných funkcí celého programu. Schopnost vytvářet malé dokonalé programy se proto jeví jako zásadní dovednost každého poctivého programátora. Tento kurz je věnován tomu, jak psát malé a při tom elegantní, ale hlavně správné a efektivní programy. Ukážeme, jak několik jednoduchých postupů a principů může k naplnění tohoto cíle stačit. Jen je třeba se s nimi seznámit a prakticky je zvládnout! Proto je převážná část kurzu zaměřena na řešení, často netradičních a zajímavých, algoritmických úloh pomocí metody elegantního programování.
Pojem procesu je fundamentálním pojmem informatiky. V oblasti komunikujících systémů hraje stejnou roli jako pojem algoritmu u sekvenčních programů. Cílem předmětu je definovat pojem procesu formálně, získat základní dovednosti, které jsou používány pro formální specifikaci a analýzu komunikujících systémů, včetně teoretických základů příslušných formálních nástrojů. Po absolvování kurzu získají studenti schopnost specifikovat a implementovat v jazyce CCS jednoduché komunikační protokoly; analyzovat a formálně ověřovat korektnost návrhu; orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení.
Předmět je zaměřen na hlubší studium výsledků teorie vyčíslitelnosti s důrazem na osvojení si používaných důkazových metod a technik. • Po skončení kurzu student porozumí základním výsledkům o vyčíslitelnosti nad nespočetnými množinami; bude schopen zhodnotit další poznatky o klasifikaci problémů, zejména aritmetické hierarchii a relativizované teorii vyčíslitelnosti.
2023 | |
---|---|
149 | N. Beneš, L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Phenotype Control of Partially Specified Boolean Networks. CMSB. |
148 | L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Temporary and permanent control of partially specified Boolean networks. Biosystems. |
147 | N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek. Boolean Network Sketches: A Unifying Framework for Logical Model Inference. Bioinformatics. |
146 | M. Troják, D. Šafránek, S. Pastva, L. Brim. Rule-based Modelling of Biological Systems Using Regulated Rewriting. Biosystems. |
2022 | |
145 | M. Troják, D. Šafránek, B. Brozmann, L. Brim. eBCSgen 2.0: Modelling and Analysis of Regulated Rule-based Systems. CMSB 2022. |
144 | L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Temporary and Permanent Control of Partially Specified Boolean Networks. BioSystems. |
143 | N. Beneš, L. Brim, O. Huvar, S. Pastva, D. Šafránek, E. Šmijáková. AEON.py: Python Library for Attractor Analysis in Asynchronous Boolean Networks. Bioinformatics. |
142 | N. Beneš, L. Brim, J. Kadlecaj, S. Pastva, D. Šafránek. Exploring Attractor Bifurcations in Boolean Networks. BMC Bioinformatics. |
141 | N. Beneš, L. Brim, S. Pastva, D. Šafránek. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. Logical Methods in Computer Science. |
2021 | |
140 | N. Beneš, L. Brim, S. Pastva, D. Šafránek. Aeon 2021: Bifurcation Decision Trees in Boolean Networks. CMSB 2021. |
139 | N. Beneš, L. Brim, S. Pastva, D. Šafránek. Computing Bottom SCCs Symbolically Using Transition Guided Reduction. CAV 2021. |
138 | L. Brim, S. Pastva, D. Šafránek, E. Šmijáková. Parallel One-Step Control of Parametrised Boolean Networks. Mathematics. |
137 | N. Beneš, L. Brim, S. Pastva, D. Šafránek. Symbolic Coloured SCC Decomposition. TACAS 2021. |
2020 | |
136 | M. Troják, D. Šafránek, L. Mertová, L. Brim. Executable Biochemical Space for Specification and Analysis of Biochemical System. Plos ONE. |
135 | M. Troják, D. Šafránek, L. Mertová, L. Brim. eBCSgen: A Software Tool for Biochemical Space Language. CMSB 2020. |
134 | E. Šmijáková, S. Pastva, D. Šafránek, L. Brim. Parameter Synthesis for Hybrid Systems from Hybrid CTL Specifications. CMSB 2020. |
133 | N. Benes, L. Brim, J. Kadlecaj, S. Pastva, D. Safranek. AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. CAV 2020. |
132 | N. Benes, L. Brim, S. Pastva, D. Safranek. Digital bifurcation analysis of internet congestion control protocols. International Journal of Bifurcation and Chaos. |
131 | M. Troják, D. Safránek, L. Mertová, L. Brim. Parameter Synthesis and Robustness Analysis of Rule-Based Models. NFM 2020. |
130 | N. Benes, L. Brim, S. Pastva, D. Safranek. Parallel Parameter Synthesis Algorithm for Hybrid CTL. Science of Computer Programming. |
2019 | |
129 | D. Safránek, M. Troják, V. Bruza, T. Vejpustek, J. Papousek, M. Demko, S. Pastva, A. Pejznoch, L. Brim. Barbaric Robustness Monitoring Revisited for STL* in Parasim. CMSB 2019. |
128 | N. Benes, L. Brim, S. Pastva, D. Safranek. Accelerating Parameter Synthesis using Semi-Algebraic Constraints. iFM 2019. |
127 | N. Benes, L. Brim, M. Geletka, S. Pastva, D. Safranek. Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks. ICFEM 2019. |
126 | N. Benes, L. Brim, S. Pastva, D. Safranek. Digital Bifurcation Analysis of TCP Dynamics. TACAS 2019. |
125 | N. Benes, L. Brim, J. Drazanova, S. Pastva, D. Safranek. Facetal Abstraction for Non-Linear Dynamical Systems Based on Delta-Decidable SMT. HSCC 2019. |
2018 | |
124 | N. Benes, L. Brim, S. Pastva, D. Safranek. Model Checking Approach to the Analysis of Biological Systems. Chapter in Automated Reasoning for Systems Biology and Medicine. Springer. |
123 | M. Troják, D. Šafránek, L. Brim, J. Šalagovič, J. Červený. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. SASB 2018. |
122 | M. Troják, J. Šalagovič, D. Šafránek, J. Červený, L. Brim, M. Hajnal. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. VEDMP 2018. |
121 | N. Benes, L. Brim, S. Pastva, D. Safranek, M. Trojak, J. Cerveny, J. Salagovic. Fully Automated Attractor Analysis of Cyanobacteria Models. ICSTCC 2018. |
2017 | |
121 | M. Ceska, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica. |
120 | N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. Discrete Bifurcation Analysis with Pithya. CMSB 2017. |
119 | J. Barnat, N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. Detecting Attractors in Biological Models with Uncertain Parameters. CMSB 2017. |
118 | N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. PITHYA: High-Performance Parameter Synthesis for Biological Models. ISMB 2017. |
117 | N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. CAV 2017. |
2016 | |
---|---|
116 | N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek. A Model Checking Approach to Discrete Bifurcation Analysis. FM 2016. |
115 | M. Hajnal, D. Šafránek, M. Demko, S. Pastva, P. Krejčí and L. Brim. Toward Modelling and Analysis of Transient and Sustained Behaviour of Signalling Pathways. HSB 2016. |
114 | M. Demko, N. Benes, L. Brim, S. Pastva, and D. Safranek. High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. CMSB 2016. |
113 | N. Benes, L. Brim, M. Demko, S. Pastva, and D. Safranek. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. ATVA 2016. |
112 | P. Rockai, J. Barnat and L. Brim. Model Checking C++ Programs with Exceptions. Science of Computer Programming. |
111 | M. Ceska, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica. |
110 | M. Ceska, P. Pilar, N. Paoletti, L. Brim, and M. Kwiatkowska. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. TACAS 2016. |
109 | J. Barnat, P. Bauch, N. Benes, L. Brim, J. Beran, T. Kratochvila: Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing. |
2015 | |
---|---|
108 | L. Brim, M. Demko, S. Pastva and D. Safranek. High-Performance Discrete Bifurcation Analysis for Piecewise-Affine Dynamical Systems. HSB 2015. |
107 | T. Ded, D. Safranek, M. Trojak, M. Klement, J. Salagovic and L. Brim. Formal Biochemical Space with Semantics in Kappa and BNGL. SASB 2015. |
106 | L. Brim, M. Ceska, M. Demko, S. Pastva and D. Safranek. Parameter Synthesis by Parallel Coloured CTL Model Checking. CMSB 2015. |
105 | L. Brim, M. Demko, S. Pastva and D. Safranek. Coloured Model Checking Approach to Parameter Synthesis for Executable Models in Synthetic Biology. VEMDP 2015. |
104 | A. Abate, M. Ceska, L. Brim, and M. Kwiatkowska. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. CAV 2015. |
2014 | |
---|---|
103 | M. Klement et al. E-cyanobacterium.org: A Web-based Platform for Systems Biology of Cyanobacteria. CMSB 2014. |
102 | P. Rockai, J. Barnat and L. Brim. Model Checking C++ with Exceptions. AVOCS 2014. |
101 | L. Brim, J. Niznan and D. Safranek. Compact Representation of Photosynthesis Dynamics by Rule-based Models. SASB 2014. |
100 | M. Ceska, D. Safranek, S. Drazan and L. Brim: Robustness Analysis of Stochastic Biochemical Systems. PLoS ONE. [url] |
99 | L. Brim, P. Dluhos, D. Safranek, T. Vejpustek. STL*: Extending signal temporal logic with signal-value freezing operator. Information and Computation, 236:52-67 (2014). [url] |
2013 | |
---|---|
98 | L. Brim and M. Ceska and S. Drazan and D. Safranek: On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking. CoRR, volume abs/1310.4734 |
97 | L. Brim, J. Fabrikova, T. Vejpustek and D. Safranek. Robustness Analysis for Value-Freezing Signal Temporal Logic. HSB 2013. |
96 | S. Van Goethem, J-M. Jacquet, L. Brim, D. Safranek. Timed Modelling of Gene Networks with Arbitrarily Precise Expression Discretization. ENTCS 293:67-81. |
95 | L. Brim, M. Ceska, S. Drazan and D. Safranek. Robustness Analysis of Stochastic Systems. CompMod 2013. |
94 | L. Brim, V. Ded and D. Safranek. Qualitative modelling and analysis of Photosystem II. BioPPN 2013. |
93 | L. Brim, M. Ceska and D. Safranek. Model Checking of Biological Systems. SFM on Design of Computer, Communication and Software Systems: Dynamical Systems. [ url] |
92 | J. Barnat, L. Brim and V. Havel. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD 2013.[url] |
91 | L. Brim, M. Ceska, S. Drazan and D. Šafránek. Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking. CAV 2013.[url] |
90 | J. Barnat, L. Brim, V. Havel, J. Havlíček, J. Kriho, M. Lenco, P. Ročkai, V. Štill and J. Weiser. DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++ Programs. CAV 2013.[ |
89 | P. Rockai, J. Barnat and L. Brim. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. NFM 2013. |
2012 | |
---|---|
88 | D. Safranek, J. Cerveny, M. Klement, L. Brim, D. Lazar and L. Nedbal: E-photosynthesis: Web-based platform for photosynthetic processes (poster). CMSB'12. |
87 | L. Brim and J. Chaloupka. Using Strategy Improvement to Stay Alive. Int. J. Found. Comput. Sci. |
86 | J. Barnat, P. Bauch, L. Brim, and M. Ceska. Designing Fast LTL Model Checking Algorithms for Many-Core GPUs. Journal of Parallel and Distributed Computing. [ url] |
85 | P. Dluhos, D. Safranek, and L. Brim. On Expressing and Monitoring Oscillatory Dynamics. HSB 2012. |
84 | L. Brim J. Fabrikova, S. Drazan and D. Safranek. On Approximative Reachability Analysis of Biochemical Dynamical Systems. Transactions on Computational Systems Biology. |
83 | J. Barnat, P. Bauch, and L. Brim. Checking Sanity of Software Requirements. SEFM 2012. |
82 | J. Barnat, L. Brim, P. Rockai, J. Beran, and T. Kratochvila. Tool Chain to support Automated Formal Verification of Avionics Simulink Designs. FMICS 2012. |
81 | S. Van Goethem, J-M. Jacquet, L. Brim and D. Safránek. Timed Modelling of Gene Networks with Arbitrary Expression Level Discretization. CS2Bio12. |
80 | J. Barnat, L. Brim, J. Beran, T. Kratochvila and R. Oliveira. Executing Model Checking Counterexamples in Simulink. TASE 2012. |
79 | J. Barnat, L. Brim, A. Krejci, A. Streck, D. Safránek, M. Vejnar, T. Vejpustek: On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Trans. Comput. Biology Bioinform. [ url]. |
78 | J. Barnat, L. Brim and P. Rockai. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NFM 2012. |
77 | J. Barnat, L. Brim, and P. Rockai:: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12). [ url] |
2011 | |
---|---|
76 | L. Brim and J. Barnat. Platform Dependent Verification: Engineering Verification Tools for 21st Century . PDMC 2011. |
75 | L. Brim, J. Fabrikova, S. Drazan and D. Safranek. Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. COMPMOD 2011. |
74 | J. Barnat, P. Bauch, L. Brim, and M. Ceska. Computing Optimal Cycle Mean in Parallel on CUDA. PDMC 2011. |
73 | L. Brim, J. Chaloupka, L. Doyen, R. Gentilini and J. F. Raskin: Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), 2011. |
72 | D. Safranek, J. Cerveny, M. Klement, J. Pospisilova, L. Brim, D. Lazar and L. Nedbal: E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes. Biosystems 103(2), 2011. |
71 | J. Barnat, P. Bauch, L. Brim, and M. Ceska. Computing Strongly Connected Components in Parallel on CUDA. IPDPS 2011. |
70 | S. Edelkamp, D. Sulewski, J. Barnat, L. Brim, and P. Simecek: Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2). |
2010 | |
---|---|
69 | J. Barnat, P. Bauch, L. Brim, and M. Ceska. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS 2010. |
68 | J. Barnat, L. Brim, D. Safranek, and M. Vejnar. Parameter Scanning by Parallel Model Checking with Applications to Systems and Synthetic Biology. HiBi 2010. |
67 | J. Barnat, L. Brim, M. Ceska, and P. Rockai. DiVinE: Parallel Distributed Model Checker. PDMC 2010. |
66 | L. Brim and J. Chaloupka. Using Strategy Improvement to Stay Alive. Gandalf 2010. |
65 | J. Barnat, L. Brim, P. Rockai: Parallel Partial Order Reduction with Topological Sort Proviso. SEFM 2010. |
64 | J. Barnat, L. Brim, P. Rockai: Scalable Multi-Core LTL Model-Checking. STTT. |
63 | J. Barnat, L. Brim and D. Safranek. High-Performance Analysis of Biological Systems Dynamics with DiVinE. Briefings in Bioinformatics, vol. 11(3). |
2009 | |
---|---|
62 | J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova and D. Safranek: On algorithmic analysis of transcriptional regulation by LTL model checking. Theor. Comput. Sci., vol. 410(33-34). |
61 | J. Chaloupka and L. Brim. Faster Algorithm for Mean-Payoff Games. MEMICS 2009. |
60 | J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova and D. Safranek. Computational Analysis of Large-Scale Multi-Affine ODE Models. HiBi 2009. |
59 | J. Barnat, L. Brim, M. Ceska: DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. PDMC 2009. |
58 | J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova , J. Lanik and D. Safranek: BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. CMSB'09. |
57 | J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek: BioDiVinE: A Framework for Parallel Analysis of Biological Models. COMPMOD 2009. |
56 | J. Barnat, L. Brim, M. Ceska, and T. Lamr: CUDA accelerated LTL Model Checking. ICPADS 2009. |
55 | J. Barnat, L. Brim, and P. Rockai: A Time-Optimal On-the-fly Parallel Algorithm for Model Checking of Weak LTL Properties. ICFEM 2009. |
54 | J. Barnat, L. Brim, and P. Rockai: DiVinE 2.0: High-Performance Model Checking. HiBi 2009. |
53 | J. Barnat, L. Brim, and P. Simecek: Cluster-Based I/O-Efficient LTL Model Checking. ASE 2009. |
52 | J. Barnat, L. Brim, and P. Simecek: Parallel I/O-Efficient State Space Generation. MASSIVE 2009. |
51 | H. Bal, J. Barnat, L. Brim, and K. Verstoep: Efficient Large-Scale Model Checking. IPDPS 2009. |
50 | N. Benes, L. Brim, I. Cerna, J. Sochor, P. Varekova and B. Zimmerova: Partial Order Reduction for State/Event LTL. IFM 2009. |
2008 | |
---|---|
49 | J. Barnat, L. Brim, I. Cerna, M. Ceska and J. Tumova: Local Quantitative LTL Model Checking. FMICS 2008. |
48 | J. Barnat, L. Brim, S. Edelkamp, D. Sulewski and P. Simecek: Can Flash Memory Help in Model Checking. FMICS 2008. |
47 | L. Brim, J. Barnat: Squeeze All the Power Out of Your Hardware to Verify Your Software! ISOLA 2008. |
46 | J. Barnat, L. Brim, P. Rockai: DiVinE Multi-Core -- A Parallel LTL Model-Checker. ATVA 2008. |
45 | J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: ProbDiVinE-MC: Multi-Core LTL Model Checker for Probabilistic Systems. QEST 2008. |
44 | J. Barnat, L. Brim, P. Simecek, M. Weber: Revisiting Resistance Speeds Up LTL Model Checking. TACAS 2008. |
2007 | |
---|---|
43 | J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek: Parallel Model Checking Large-Scale Genetic Regulatory Network with DIVINE. FBTC 2007. |
42 | J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: ProbDiVinE - A Parallel Qualitative LTL Model-Checker. QEST 2007. |
41 | L. Brim, J. Barnat: Tutorial on Parallel Model-Checking. SPIN 2007. |
40 | J. Barnat, L. Brim, P. Rockai: Scalable Multi-Core LTL Model-Checking. SPIN 2007. |
39 | J. Barnat, L. Brim, M. Leucker: Parallel Model Checking and the FMICS-jETI Platform. ICECCS 2007. |
38 | J. Barnat, L. Brim, P. Simecek: I/O Efficient Accepting Cycle Detection. CAV 2007. |
37 | L. Brim, M. Kretinsky: Model Checking Large Finite-State Systems and Beyond. SOFSEM 2007. |
2006 | |
---|---|
36 | J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova: Distributed Qualitative LTL Model Checking of Markov Decision Processes. PDMC 2006. |
35 | L. Brim, I. Cerna, P. Moravec, J. Simsa: On Combining Partial Order Reduction with Fairness Assumptions. FMICS 2006. |
34 | L. Brim: Distributed Verification: Exploring the Power of Raw Computing Power. PDMC 2006. |
33 | J. Barnat, L. Brim, I. Cerna, P. Moravec, P. Rockai, P. Simecek: DiVinE - The Distributed Verification Environment. CAV 2006. |
32 | Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. Electr. Notes Theor. Comput. Sci. 135 (2): 3-18 (2006) |
2005 | |
---|---|
31 | Jiri Barnat, Lubos Brim, Ivana Cerna: Distributed Analysis of Large Systems. FMCO 2005. |
30 | Barbora Zimmerova, Lubos Brim, Ivana Cerna, Pavlina Varekova: Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. SAVCBS 2005. |
29 | Radek Pelanek, Tomas Hanzl, Ivana Cerna, Lubos Brim: Enhancing Random Walk State Space Exploration. FMICS 2005. |
28 | Jiri Barnat, Lubos Brim, Ivana Cerna, Pavel Simecek: DiVinE - The Distributed Verification Environment. PDMC 2005. |
27 | Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. PDMC 2005. |
26 | Jiri Barnat, Lubos Brim and Jakub Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. ENTCS 133(1): (2005) |
25 | Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Distributed Partial Order Reduction of State Spaces. ENTCS 128(3): (2005) |
24 | Lubos Brim, Orna Grumberg: Introductory Paper: Parallel and Distributed Model-Checking. International Journal on Software Tools for Technology Transfer, Feb. 2005 |
23 | Lubos Brim, Karen Yorav, Jitka Zidkova: Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer, Feb. 2005 |
2004 | |
---|---|
22 | Lubos Brim, Ivana Cerna, Lukas Hejtmanek: Distributed Negative Cycle Detection Algorithms. In Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Elsevier B.V., 2004. |
21 | Jiri Barnat, Lubos Brim, Jakub Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. FMICS 2004. |
20 | Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Distributed Partial Order Reduction of State Spaces. PDMC 2004. |
19 | Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. FMCAD 2004. |
18 | Lubos Brim: Parallel Model-Checking. ERCIM News, number 58, July 2004. |
2003 | |
---|---|
17 | Jiri Barnat, Lubos Brim, Jakub Chaloupka: Parallel Breadth-First Search LTL Model-Checking. ASE 2003. |
16 | Lubos Brim, Orna Grumberg: Preface. ENTCS 89(1): (2003) |
15 | Lubos Brim, Jitka Zidkova: Using Assumptions to Distribute Alternation Free Mu-Calculus Model Checking. PDMC 2003 (ENTCS 89.1). |
14 | Lubos Brim, Ivana Cerna, Lukas Hejtmanek: Distributed Negative Cycle Detection Algorithms. PARCO 2003. |
13 | Lubos Brim, Mojmír Kretínský, Jean-Marie Jacquet, David Gilbert: Modelling Multi-Agent Systems as Synchronous Concurrent Constraint Processes. Computing and Informatics, Vol. 21, 2002. |
12 | Lubos Brim, Jiri Barnat: Distribution of Explicit-State LTL Model-Checking. FMICS 2003 (ENTCS 80). |
11 | Jean-Marie Jacquet, Lubos Brim, David Gilbert, Mojmír Kretínský: Coordination by Means of Synchronous and Asynchronous Communication in Concurrent Constraint Programming. ENTCS 68(3): (2003) |
2002 | |
---|---|
10 | Lubos Brim: Automated Formal Verification. EurOpen 2002. |
9 | Jiri Barnat, Lubos Brim, Ivana Cerna: Property Driven Distribution of Nested DFS. VCL'02. |
8 | Lubos Brim, Petr Jancar, Mojmír Kretínský, Antonín Kucera: CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Springer 2002 |
7 | Lubos Brim, Orna Grumberg: Preface. ENTCS 68(4): (2002) |
6 | Lubos Brim, Jitka Crhova, Karen Yorav: Using Assumptions to Distribute CTL Model Checking. ENTCS 68(4): (2002) |
2001 | |
---|---|
5 | Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: Distributed LTL Model Checking Based on Negative Cycle Detection. FSTTCS 2001: 96-107 |
4 | Lubos Brim, Ivana Cerna, Martin Necesal: Randomization Helps in LTL Model Checking. PAPM-PROBMIV 2001: 105-119 |
3 | Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: How to Employ Reverse Search in Distributed Single Source Shortest Paths. SOFSEM 2001: 191-200 |
2 | Lubos Brim, David Gilbert, Jean-Marie Jacquet, Mojmír Kretínský: Multi-agent Systems as Concurrent Constraint Processes. SOFSEM 2001: 201-210 |
1 | Jiri Barnat, Lubos Brim, Jitka Stríbrná: Distributed LTL Model-Checking in SPIN. SPIN 2001: 200-216 |