list of all publications

2018
126 M. Hajnal, S. Pastva. Toward Model Selection by Formal Methods. SASB 2018.
125 N. Beneš, L. Brim, S. Pastva, D. Šafránek. Computer-Aided Formal Analysis of Biomedical Systems. Chapter in Automated Reasoning for Systems Biology and Medicine.
124 M. Troják, D. Šafránek, L. Brim, J. Šalagovič, J. Červený. Executable Biochemical Space for Specification and Analysis of Biochemical Systems. SASB 2018.
123 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.
122 N. Beneš, L. Brim, S. Pastva, D. Šafránek, M. Troják, J. Červený, J. Šalagovič. Fully Automated Attractor Analysis of Cyanobacteria Models. ICSTCC 2018.
2017
121 M. Češka, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica.
120 N. Beneš, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Šafránek. Discrete Bifurcation Analysis with Pithya. CMSB 2017.
119 J. Barnat, N. Beneš, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Šafránek. Detecting Attractors in Biological Models with Uncertain Parameters. CMSB 2017.
118 N. Beneš, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Šafránek. PITHYA: High-Performance Parameter Synthesis for Biological Models. ISMB 2017.
117 N. Beneš, L. Brim, M. Demko, S. Pastva and D. Šafránek. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. CAV 2017.
2016
116 M. Troják, D. Šafránek, J. Hrabec, J. Šalagovič, F. Romanovská, J. Červený. E-cyanobacterium.org: A web-based platform for systems biology of cyanobacteria. CMSB 2016.
115 N. Beneš, L. Brim, M. Demko, S. Pastva and D. Šafránek. A Model Checking Approach to Discrete Bifurcation Analysis. FM 2016.
114 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.
113 M. Demko, N. Beneš, L. Brim, S. Pastva, and D. Šafránek. High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. CMSB 2016.
112 N. Beneš, L. Brim, M. Demko, S. Pastva, and D. Šafránek. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. ATVA 2016.
111 P. Ročkai, J. Barnat and L. Brim. Model Checking C++ Programs with Exceptions. Science of Computer Programming.
110 M. Češka, 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. Beneš, 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. Šafránek. High-Performance Discrete Bifurcation Analysis for Piecewise-Affine Dynamical Systems. HSB 2015.
107 T. Ded, D. Šafránek, M. Troják, M. Klement, J. Šalagovič and L. Brim. Formal Biochemical Space with Semantics in Kappa and BNGL. SASB 2015.
106 L. Brim, M. Češka, M. Demko, S. Pastva and D. Šafránek. Parameter Synthesis by Parallel Coloured CTL Model Checking. CMSB 2015.
105 L. Brim, M. Demko, S. Pastva and D. Šafránek. Coloured Model Checking Approach to Parameter Synthesis for Executable Models in Synthetic Biology. VEMDP 2015.
104 A. Abate, M. Češka, 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. Ročkai, J. Barnat and L. Brim. Model Checking C++ with Exceptions. AVOCS 2014.
101 L. Brim, J. Nižnan and D. Šafránek. Compact Representation of Photosynthesis Dynamics by Rule-based Models. SASB 2014.
100 M. Češka, D. Šafránek, S. Dražan and L. Brim: Robustness Analysis of Stochastic Biochemical Systems. PLoS ONE. [url]
99 L. Brim, P. Dluhoš, D. Šafránek, 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. Češka and S. Dražan and D. Šafránek: On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking. CoRR, volume abs/1310.4734
97 L. Brim, J. Fabriková, T. Vejpustek and D. Šafránek. Robustness Analysis for Value-Freezing Signal Temporal Logic. HSB 2013.
96 S. Van Goethem, J-M. Jacquet, L. Brim, D. Šafránek. Timed Modelling of Gene Networks with Arbitrarily Precise Expression Discretization. ENTCS 293:67-81.
95 L. Brim, M. Češka, S. Dražan and D. Šafránek. Robustness Analysis of Stochastic Systems. CompMod 2013.
94 L. Brim, V. Děd and D. Šafránek. Qualitative modelling and analysis of Photosystem II. BioPPN 2013.
93 L. Brim, M. Češka and D. Šafránek. 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. Češka, S. Dražan 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. Lenčo, P. Ročkai, V. Štill and J. Weiser. DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++ Programs. CAV 2013.[
89 P. Ročkai, J. Barnat and L. Brim. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. NFM 2013.
2012
88 D. Šafránek, 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. Češka. Designing Fast LTL Model Checking Algorithms for Many-Core GPUs. Journal of Parallel and Distributed Computing. [ url]
85 P. Dluhos, D. Šafránek, and L. Brim. On Expressing and Monitoring Oscillatory Dynamics. HSB 2012.
84 L. Brim J. Fabrikova, S. Drazan and D. Šafránek. 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. Ročkai, 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. Šafrá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. Šafrá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. Ročkai. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NFM 2012.
77 J. Barnat, L. Brim, and P. Ročkai:: 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. Šafránek. Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. COMPMOD 2011.
74 J. Barnat, P. Bauch, L. Brim, and M. Češka. 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. Šafránek, 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. Češka. Computing Strongly Connected Components in Parallel on CUDA. IPDPS 2011.
70 S. Edelkamp, D. Sulewski, J. Barnat, L. Brim, and P. Šimeček: Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2).
2010
69 J. Barnat, P. Bauch, L. Brim, and M. Češka. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. ICPADS 2010.
68 J. Barnat, L. Brim, D. Šafránek, and M. Vejnar. Parameter Scanning by Parallel Model Checking with Applications to Systems and Synthetic Biology. HiBi 2010.
67 J. Barnat, L. Brim, M. Češka, and P. Ročkai. 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. Ročkai: Parallel Partial Order Reduction with Topological Sort Proviso. SEFM 2010.
64 J. Barnat, L. Brim, P. Ročkai: Scalable Multi-Core LTL Model-Checking. STTT.
63 J. Barnat, L. Brim and D. Šafránek. High-Performance Analysis of Biological Systems Dynamics with DiVinE. Briefings in Bioinformatics, vol. 11(3).
2009
62 J. Barnat, L. Brim, I. Černá, S. Drazan, J. Fabrikova and D. Šafránek: 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. Černá, S. Drazan, J. Fabrikova and D. Šafránek. Computational Analysis of Large-Scale Multi-Affine ODE Models. HiBi 2009.
59 J. Barnat, L. Brim, M. Češka: DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. PDMC 2009.
58 J. Barnat, L. Brim, I. Černá, S. Drazan, J. Fabrikova , J. Lanik and D. Šafránek: BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. CMSB'09.
57 J. Barnat, L. Brim, I. Černá, S. Drazan, J. Fabrikova, D. Šafránek: BioDiVinE: A Framework for Parallel Analysis of Biological Models. COMPMOD 2009.
56 J. Barnat, L. Brim, M. Češka, and T. Lamr: CUDA accelerated LTL Model Checking. ICPADS 2009.
55 J. Barnat, L. Brim, and P. Ročkai: A Time-Optimal On-the-fly Parallel Algorithm for Model Checking of Weak LTL Properties. ICFEM 2009.
54 J. Barnat, L. Brim, and P. Ročkai: DiVinE 2.0: High-Performance Model Checking. HiBi 2009.
53 J. Barnat, L. Brim, and P. Šimeček: Cluster-Based I/O-Efficient LTL Model Checking. ASE 2009.
52 J. Barnat, L. Brim, and P. Šimeček: 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. Beneš, L. Brim, I. Černá, J. Sochor, P. Varekova and B. Zimmerova: Partial Order Reduction for State/Event LTL. IFM 2009.
2008
49 J. Barnat, L. Brim, I. Černá, M. Češka and J. Tumova: Local Quantitative LTL Model Checking. FMICS 2008.
48 J. Barnat, L. Brim, S. Edelkamp, D. Sulewski and P. Šimeček: 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. Ročkai: DiVinE Multi-Core -- A Parallel LTL Model-Checker. ATVA 2008.
45 J. Barnat, L. Brim, I. Černá, M. Češka, J. Tumova: ProbDiVinE-MC: Multi-Core LTL Model Checker for Probabilistic Systems. QEST 2008.
44 J. Barnat, L. Brim, P. Šimeček, M. Weber: Revisiting Resistance Speeds Up LTL Model Checking. TACAS 2008.
2007
43 J. Barnat, L. Brim, I. Černá, S. Drazan, D. Šafránek: Parallel Model Checking Large-Scale Genetic Regulatory Network with DIVINE. FBTC 2007.
42 J. Barnat, L. Brim, I. Černá, M. Češka, 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. Ročkai: 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. Šimeček: 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. Černá, M. Češka, J. Tumova: Distributed Qualitative LTL Model Checking of Markov Decision Processes. PDMC 2006.
35 L. Brim, I. Černá, P. Moravec, J. Šimša: 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. Černá, P. Moravec, P. Ročkai, P. Šimeček: DiVinE - The Distributed Verification Environment. CAV 2006.
32L. Brim, I. Černá, P. Moravec, J. Šimša: 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 J. Barnat, L. Brim, I. Černá: Distributed Analysis of Large Systems. FMCO 2005.
30 B. Zimmerova, L. Brim, I. Černá, P. Varekova: Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. SAVCBS 2005.
29 R. Pelánek, T. Hanžl, I. Černá, L. Brim: Enhancing Random Walk State Space Exploration. FMICS 2005.
28 J. Barnat, L. Brim, I. Černá, P. Šimeček: DiVinE - The Distributed Verification Environment. PDMC 2005.
27 L. Brim, I. Černá, P. Moravec, J. Šimša: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. PDMC 2005.
26J. Barnat, L. Brim and J. Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. ENTCS 133(1): (2005)
25L. Brim, I. Černá, P. Moravec, J. Šimša: Distributed Partial Order Reduction of State Spaces. ENTCS 128(3): (2005)
24L. Brim, Orna Grumberg: Introductory Paper: Parallel and Distributed Model-Checking. International Journal on Software Tools for Technology Transfer, Feb. 2005
23L. Brim, K. Yorav, J. Zidkova: Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer, Feb. 2005
2004
22L. Brim, I. Černá, L. Hejtmánek: Distributed Negative Cycle Detection Algorithms. In Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Elsevier B.V., 2004.
21 J. Barnat, L. Brim, J. Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. FMICS 2004.
20L. Brim, I. Černá, P. Moravec, J. Šimša: Distributed Partial Order Reduction of State Spaces. PDMC 2004.
19 L. Brim, I. Černá, P. Moravec, J. Šimša: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. FMCAD 2004.
18L. Brim: Parallel Model-Checking. ERCIM News, number 58, July 2004.
2003
17 J. Barnat, L. Brim, J. Chaloupka: Parallel Breadth-First Search LTL Model-Checking. ASE 2003.
16L. Brim, O. Grumberg: Preface. ENTCS 89(1): (2003)
15L. Brim, J. Zidkova: Using Assumptions to Distribute Alternation Free Mu-Calculus Model Checking. PDMC 2003 (ENTCS 89.1).
14L. Brim, I. Černá, L. Hejtmanek: Distributed Negative Cycle Detection Algorithms. PARCO 2003.
13L. Brim, M. Kretínský, J-M. Jacquet, D. Gilbert: Modelling Multi-Agent Systems as Synchronous Concurrent Constraint Processes. Computing and Informatics, Vol. 21, 2002.
12L. Brim, J. Barnat: Distribution of Explicit-State LTL Model-Checking. FMICS 2003 (ENTCS 80).
11Jean-Marie Jacquet, L. Brim, D. Gilbert, M. Kretínský: Coordination by Means of Synchronous and Asynchronous Communication in Concurrent Constraint Programming. ENTCS 68(3): (2003)
2002
10L. Brim: Automated Formal Verification. EurOpen 2002.
9J. Barnat, L. Brim, I. Černá: Property Driven Distribution of Nested DFS. VCL'02.
8L. Brim, P. Jančar, M. Kretínský, A. Kučera: CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings. Springer 2002
7L. Brim, Orna Grumberg: Preface. ENTCS 68(4): (2002)
6L. Brim, J. Crhova, K. Yorav: Using Assumptions to Distribute CTL Model Checking. ENTCS 68(4): (2002)
2001
5L. Brim, I. Černá, P. Krcál, Radek Pelánek: Distributed LTL Model Checking Based on Negative Cycle Detection. FSTTCS 2001: 96-107
4L. Brim, I. Černá, Martin Necesal: Randomization Helps in LTL Model Checking. PAPM-PROBMIV 2001: 105-119
3L. Brim, I. Černá, P. Krcál, Radek Pelánek: How to Employ Reverse Search in Distributed Single Source Shortest Paths. SOFSEM 2001: 191-200
2L. Brim, D. Gilbert, Jean-Marie Jacquet, M. Kretínský: Multi-agent Systems as Concurrent Constraint Processes. SOFSEM 2001: 201-210
1J. Barnat, L. Brim, J. Stríbrná: Distributed LTL Model-Checking in SPIN. SPIN 2001: 200-216
Top