Highlights

April 1, 2010
Artemis Joint Undertaking project iFEST has been officially lounched.

MU is a partner in the new top ranked Artemis project, focusing on integrated tool chains for embedded systems development.

The iFEST project has 20 partners and is coordinated by ABB. The project runs for three years with a total budget of 16 MegaEuro. The proposal was ranked no. 1 in the Artemis proposal evaluation for the 2nd call!

www.artemis-ifest.eu

Contact Info




Luboš Brim
Faculty of Informatics
Masaryk University
Botanicka 68a
602 00 BRNO
Czech Republic

Tel: +420 549 493 647
Fax: +420 549 491 820
brim at fi dot muni dot cz

Selected Publications since 2001

new DBLP - DBLP - ACM DL - Google Scholar - Microsoft Academic Search | Home

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.  
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. 
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.  
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. 
26Jiri Barnat, Lubos Brim and Jakub Chaloupka: From Distributed Memory Cycle Detection to Parallel LTL Model Checking. ENTCS 133(1): (2005)
25Lubos Brim, Ivana Cerna, Pavel Moravec, Jiri Simsa: Distributed Partial Order Reduction of State Spaces. ENTCS 128(3): (2005)
24Lubos Brim, Orna Grumberg: Introductory Paper: Parallel and Distributed Model-Checking. International Journal on Software Tools for Technology Transfer, Feb. 2005
23Lubos 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.
16Lubos Brim, Orna Grumberg: Preface. ENTCS 89(1): (2003)
15Lubos 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. 
12Lubos Brim, Jiri Barnat: Distribution of Explicit-State LTL Model-Checking. FMICS 2003 (ENTCS 80).
11Jean-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. 
9Jiri 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 
7Lubos Brim, Orna Grumberg: Preface. ENTCS 68(4): (2002)
6Lubos Brim, Jitka Crhova, Karen Yorav: Using Assumptions to Distribute CTL Model Checking. ENTCS 68(4): (2002)
2001
5Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: Distributed LTL Model Checking Based on Negative Cycle Detection. FSTTCS 2001: 96-107
4Lubos Brim, Ivana Cerna, Martin Necesal: Randomization Helps in LTL Model Checking. PAPM-PROBMIV 2001: 105-119
3Lubos Brim, Ivana Cerna, Pavel Krcál, Radek Pelánek: How to Employ Reverse Search in Distributed Single Source Shortest Paths. SOFSEM 2001: 191-200
2Lubos Brim, David Gilbert, Jean-Marie Jacquet, Mojmír Kretínský: Multi-agent Systems as Concurrent Constraint Processes. SOFSEM 2001: 201-210
1Jiri Barnat, Lubos Brim, Jitka Stríbrná: Distributed LTL Model-Checking in SPIN. SPIN 2001: 200-216

Copyright © 2009 Luboš Brim. All Rights Reserved.