Luboš Brim - Publications

Selected Publications since 2001

2017
120		M. Ceska, F. Danneberg, N. Paoletti, L. Brim, and M. Kwiatkowska. Precise Parameter Synthesis for Stochastic Biochemical Systems. Acta Informatica.
119		N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. Discrete Bifurcation Analysis with Pithya. CMSB 2017.
118		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.
117		N. Benes, L. Brim, M. Demko, M. Hajnal, S. Pastva and D. Safranek. PITHYA: High-Performance Parameter Synthesis for Biological Models. ISMB 2017.
116		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
115		N. Benes, L. Brim, M. Demko, S. Pastva and D. Safranek. 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. Benes, L. Brim, S. Pastva, and D. Safranek. High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. CMSB 2016.
112		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.
111		P. Rockai, J. Barnat and L. Brim. Model Checking C++ Programs with Exceptions. Science of Computer Programming.
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, [bibtex, pdf]
97		L. Brim, J. Fabrikova, T. Vejpustek and D. Safranek. Robustness Analysis for Value-Freezing Signal Temporal Logic. HSB 2013.[bibtex, pdf]
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.[bibtex, pdf, url]
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.[bibtex, url]
93		L. Brim, M. Ceska and D. Safranek. Model Checking of Biological Systems. SFM on Design of Computer, Communication and Software Systems: Dynamical Systems. [bibtex, pdf, url]
92		J. Barnat, L. Brim and V. Havel. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. ACSD 2013.[bibtex, pdf, 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.[bibtex, pdf, 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.[bibtex, pdf]
89		P. Rockai, J. Barnat and L. Brim. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. NFM 2013.[bibtex, pdf]
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. [bibtex, pdf, 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. [bibtex, pdf]
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. [bibtex, pdf]
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. [bibtex, pdf]
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. [bibtex, pdf, url].
78		J. Barnat, L. Brim and P. Rockai. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. NFM 2012. [bibtex, pdf]
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). [bibtex, pdf, url]
2011
76		L. Brim and J. Barnat. Platform Dependent Verification: Engineering Verification Tools for 21st Century . PDMC 2011. [bibtex, pdf]
75		L. Brim, J. Fabrikova, S. Drazan and D. Safranek. Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation. COMPMOD 2011. [bibtex, pdf, url]
74		J. Barnat, P. Bauch, L. Brim, and M. Ceska. Computing Optimal Cycle Mean in Parallel on CUDA. PDMC 2011. [bibtex, pdf, url]
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. [bibtex, pdf]
70		S. Edelkamp, D. Sulewski, J. Barnat, L. Brim, and P. Simecek: Flash memory efficient LTL model checking. Sci. Comput. Program. 76(2). [bibtex, url]
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