Luboš Brim

2014

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Model Checking C++ with Exceptions,
Automated Verification of Critical Systems, 2014. [bibtex, url]

2013

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868. [bibtex, url]

Luboš Brim, Milan Češka, Sven Dražan, and David Šafránek:
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking,
Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Springer Berlin Heidelberg, 2013, 107–123. [bibtex, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Improved State Space Reductions for LTL Model Checking of C & C++ Programs,
NASA Formal Methods (NFM 2013), Springer, 2013, volume 7871 of LNCS, 1–15. [bibtex]

Jiří Barnat, Luboš Brim, and Vojtěch Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model,
Application of Concurrency to System Design (ACSD), IEEE, 2013, 51–59. [bibtex, url]

Luboš Brim, Milan Češka, and David Šafránek:
Model Checking of Biological Systems,
Formal Methods for Dynamical Systems: 13th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2013, Bertinoro, Italy, June 17-22, 2013. Advanced Lectures, Springer Berlin Heidelberg, 2013, 63–112. [bibtex, url]

Luboš Brim, Milan Češka, Sven Dražan, and David Šafránek:
On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking,
arXiv preprint arXiv:1310.4734, 2013. [bibtex]

Luboš Brim, Vilém Děd, and David Šafránek:
Qualitative modelling and analysis of Photosystem II,
CEUR Workshop Proceedings, Neuveden, 2013, 17-29. [bibtex, url]

Luboš Brim, Tomáš Vejpustek, David Šafránek, and Jana Fabriková:
Robustness Analysis for Value-Freezing Signal Temporal Logic,
Proceedings HSB 2013, Neuveden, 2013, 20-36. [bibtex, url]

S. Van Goethem, J. M. Jacquet, Luboš Brim, and David Šafránek:
Timed Modelling of Gene Networks with Arbitrarily Precise Expression Discretization,
Electron. Notes Theor. Comput. Sci., Elsevier Science Publishers B. V., 2013, 67–81. [bibtex, url]

2012

Jiří Barnat, Petr Bauch, and Luboš Brim:
Checking Sanity of Software Requirements,
Software Engineering and Formal Methods: 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 48–62. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Designing Fast LTL Model Checking Algorithms for Many-core GPUs,
Journal of Parallel and Distributed Computing, 2012. [bibtex, url]

Jiří Barnat, Luboš Brim, Jan Beran, Tomáš Kratochvíla, and Italo Romani de Oliveira:
Executing Model Checking Counterexamples in Simulink,
IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering, IEEE Computer Society, 2012, 245-248. [bibtex]

Jiří Barnat, Luboš Brim, Adam Krejci, Adam Streck, David Šafránek, Martin Vejnár, and Tomáš Vejpustek:
On Parameter Synthesis by Parallel Model Checking,
IEEE/ACM Trans. Comput. Biol. Bioinformatics, IEEE Computer Society Press, 2012, 693–705. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties,
Science of Computer Programming, Elsevier North-Holland, Inc., 2012, 1272–1288. [bibtex, url]

Jiří Barnat, Jan Beran, Luboš Brim, Kratochvíla Tomáš, and Ročkai Petr:
Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs,
Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 78–92. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs,
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, Springer Berlin Heidelberg, 2012, 252–266. [bibtex, url]

2011

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Computing Optimal Cycle Mean in Parallel on CUDA,
Electronic Proceedings in Theoretical Computer Science, 2011. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Ceška:
Computing Strongly Connected Components in Parallel on CUDA,
Parallel Distributed Processing Symposium (IPDPS), 2011 IEEE International, 2011, 544-555. [bibtex, url]

Stefan Edelkamp, Damian Sulewski, Jiří Barnat, Luboš Brim, and Pavel Šimeček:
Flash memory efficient LTL model checking,
Science of Computer Programming, 2011. [bibtex, url]

Nikola Beneš, Luboš Brim, Barbora Bühnová, Ivana Černá, Jiří Sochor, and Pavlína Moravcová Vařeková:
Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata,
Science of Computer Programming, 2011. [bibtex, url]

Luboš Brim and Jiří Barnat:
Platform Dependent Verification: On Engineering Verification Tools for 21st Century,
Electronic Proceedings in Theoretical Computer Science, 2011. [bibtex, url]

Luboš Brim, Jana Fabriková, Sven Dražan, and David Šafránek:
Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation,
Electronic Proceedings in Theoretical Computer Science, 2011. [bibtex, url]

2010

Jiří Barnat, Luboš Brim, Milan Češka, and Petr Ročkai:
DiVinE: Parallel Distributed Model Checker,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, 2010, 4–7. [bibtex, url]

Jiří Barnat, Petr Bauch, Luboš Brim, and Milan Češka:
Employing Multiple CUDA Devices to Accelerate LTL Model Checking,
16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE, 2010. [bibtex]

Jiří Barnat, Luboš Brim, and David Šafránek:
High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker,
Briefings in Bioinformatics, 2010, 301–312. [bibtex, url]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Parallel Partial Order Reduction with Topological Sort Proviso,
Proceeding of SEFM 2010, IEEE Computer Society Press, 2010. [bibtex]

Jiří Barnat, Luboš Brim, David Šafránek, and Martin Vejnár:
Parameter Scanning by Parallel Model Checking with Applications in Systems Biology,
Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010), IEEE, 2010. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Shared Memory LTL Model Checking,
International Journal on Software Tools for Technology Transfer (STTT), 2010, 139–153. [bibtex, url]

2009

Jiří Barnat, Luboš Brim, and Petr Ročkai:
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties,
Formal Methods and Software Engineering (ICFEM 2009), Springer, 2009, volume 5885 of LNCS, 407–425. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, David Šafránek, and Hongwu Ma:
BioDiVinE: A Framework for Parallel Analysis of Biological Models,
Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), 2009, 31–45. [bibtex, url]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, Jan Láník, and David Šafránek:
BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models,
Proceedings of The 7th Conference on Computational Methods in Systems Biology (CMSB’09), Universita di Pisa, 2009, volume TR-09-09 of Technical Report, 1–5. [bibtex]

Jiří Barnat, Luboš Brim, Milan Češka, and Tomáš Lamr:
CUDA accelerated LTL Model Checking,
15th International Conference on Parallel and Distributed Systems (ICPADS 2009), IEEE Computer Society, 2009, 34–41. [bibtex]

Jiří Barnat, Luboš Brim, and Pavel Šimeček:
Cluster-Based I/O Efficient LTL Model Checking,
24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), IEEE Computer Society, 2009, 635–639. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, and David Šafránek:
Computational Analysis of Large-Scale Multi-Affine ODE Models,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 81–90. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE 2.0: High-Performance Model Checking,
2009 International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 31–32. [bibtex]

Jiří Barnat, Luboš Brim, and Milan Češka:
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking,
Electronic Proceedings in Theoretical Computer Science (PDMC 2009), 2009, 107–111. [bibtex, url]

Kees Verstoep, Henri Bal, Jiří Barnat, and Luboš Brim:
Efficient Large-Scale Model Checking,
23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009), IEEE, 2009. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
Local Quantitative LTL Model Checking,
Formal Methods for Industrial Critical Systems, Springer Berlin / Heidelberg, 2009, 53-68. [bibtex, url]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, Jana Fabriková, and David Šafránek:
On algorithmic analysis of transcriptional regulation by LTL model checking,
Theor. Comput. Sci., 2009, 3128–3148. [bibtex, url]

Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, and Barbora Zimmerová:
Partial Order Reduction for State/Event LTL,
Proceedings of the International Conference on Integrated Formal Methods (IFM’09), Springer-Verlag, 2009, volume 5423 of LNCS, 307–321. [bibtex]

2008

Jiří Barnat, Luboš Brim, Stefan Edelkamp, Damian Sulewski, and Pavel Šimeček:
Can Flash Memory Help in Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 150–165. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
DiVinE Multi-Core – A Parallel LTL Model-Checker,
Automated Technology for Verification and Analysis (ATVA 2008), Springer, 2008, volume 5311 of LNCS, 234–239. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks,
Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation, Ivana Černá and Gerald Luettgen, 2008, 83-96. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
Local Quantitative LTL Model Checking,
Formal Methods for Industrial Critical Systems (FMICS 2008), Springer-Verlag, 2008, volume 5596 of LNCS, 53–68. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE,
ENTCS, Elsevier, 2008, volume 194 of ENTCS, 35–50. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems,
QEST ’08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, IEEE Computer Society, 2008, 77–78. [bibtex, url]

Jiří Barnat, Luboš Brim, Pavel Šimeček, and Michael Weber:
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking,
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)., Springer, 2008, volume 4963 of LNCS, 48–62. [bibtex]

Luboš Brim and Jiří Barnat:
Squeeze All the Power Out of Your Hardware to Verify Your Software!,
ISOLA 2008, Springer Verlag, 2008, volume 17 of CCIS, 604–618. [bibtex]

Nikola Beneš, Luboš Brim, Ivana Černá, Jiří Sochor, Pavlína Vařeková, and Barbora Zimmerová:
The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems,
Proceedings of the Workshop on Formal Aspects of Component Software (FACS’08), 2008, 221–225. [bibtex]

Barbora Zimmerová, Pavlína Vařeková, Nikola Beneš, Ivana Černá, Luboš Brim, and Jiří Sochor:
The Common Component Modeling Example: Comparing Software Component Models,
Springer-Verlag, 2008, volume 5153 of LNCS, 146–176. [bibtex]

2007

Luboš Brim:
Distributed Verification: Exploring the Power of Raw Computing Power ,
Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers, Springer Berlin Heidelberg, 2007, 23–34. [bibtex, url]

Jiří Barnat, Luboš Brim, and Pavel Šimeček:
I/O Efficient Accepting Cycle Detection,
Computer Aided Verification, Springer, 2007, volume 4590 of LNCS, 281–293. [bibtex]

Luboš Brim and Mojmír Křetínský:
Model Checking Large Finite-State Systems and Beyond,
33rd Conference on Current Trends in Theory and Practice of Computer Science, Springer-Verlag, 2007, 9-28. [bibtex]

Luboš Brim, Ivana Černá, Pavel Moravec, and Jiří Šimša:
On Combining Partial Order Reduction with Fairness Assumptions,
FMICS/PDMC, 2007, volume 4346 of Lecture Notes in Computer Science, 84–99. [bibtex]

Jiří Barnat, Luboš Brim, and Martin Leucker:
Parallel Model Checking and the FMICS-jETI Platform,
The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society Press, 2007. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Sven Dražan, and David Šafránek:
Parallel Model-Checking Genetic Regulatory Networks,
Towards Systems Biology, Verimag, 2007. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, and Jana Tůmová:
ProbDiVinE: A Parallel Qualitative LTL Model Checker,
Fourth International Conference on the Quantitative Evaluation of Systems (QEST’07), IEEE Computer Society, 2007, 215–216. [bibtex]

Jiří Barnat, Luboš Brim, and Petr Ročkai:
Scalable Multi-core LTL Model-Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 187–203. [bibtex]

Luboš Brim and Jiří Barnat:
Tutorial: Parallel Model Checking,
Model Checking Software, Springer, 2007, volume 4595 of LNCS, 2–3. [bibtex]

2006

Jiří Barnat, Luboš Brim, and Ivana Černá:
Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, Springer, 2006, 259-279. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai, and Pavel Šimeček:
DiVinE – A Tool for Distributed Verification (Tool Paper),
Computer Aided Verification, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278–281. [bibtex]

Luboš Brim, Ivana Černá, Pavel Moravec, and Jiří Šimša:
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,
Electronic Notes in Theoretical Computer Science, 2006, 3–18. [bibtex, url]

2005

Jiří Barnat, Luboš Brim, and Ivana Černá:
Cluster-Based LTL Model Checking of Large Systems,
Formal Methods for Components and Objects, 2005, 259–279. [bibtex]

Barbora Zimmerová, Luboš Brim, Ivana Černá, and Pavlína Vařeková:
Component-Interaction Automata as a Verification-Oriented Component-Based System Specification,
Specification and Verification of Component-Based Systems (SAVCBS 05), 2005, 31-38. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, and Pavel Šimeček:
DiVinE The Distributed Verification Environment,
4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’05), 2005. [bibtex]

Jiří Barnat, Luboš Brim, Ivana Černá, and Pavel Šimeček:
DiVinE – The Distributed Verification Environment,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 89–94. [bibtex]

Luboš Brim, Ivana Černá, Pavel Moravec, and Jiří Šimša:
Distributed Partial Order Reduction,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2005, 63–74. [bibtex]

Radek Pelánek, Tomáš Hanžl, Ivana Černá, and Luboš Brim:
Enhancing Random Walk State Space Exploration,
Tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 05), ACM Press, 2005, 98–105. [bibtex]

Jiří Barnat, Luboš Brim, and Jakub Chaloupka:
From Distributed Memory Cycle Detection to Parallel LTL Model Checking,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2005, 21–39. [bibtex]

Luboš Brim, Ivana Černá, Pavel Moravec, and Jiří Šimša:
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,
Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), TU Munchen, 2005, 1-12. [bibtex]

2004

Luboš Brim, Ivana Černá, Pavel Moravec, and Jiří Šimša:
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking,
Formal Methods in Computer-Aided Design (FMCAD), Springer, 2004, volume 3312 of LNCS, 352-366. [bibtex, pdf]

Luboš Brim, Ivana Černá, and Lukáš Hejtmánek:
Distributed Negative Cycle Detection Algorithms,
Parallel Computing: Software Technology, Algorithms, Architectures & Applications, Elsevier V.B., 2004, volume 13 of Advances in Parallel Computing, 297 – 305. [bibtex]

2003

Luboš Brim and Jiří Barnat:
Distribution of Explicit-State LTL Model-Checking,
8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science. [bibtex]

Luboš Brim, Ivana Černá, and Lukáš Hejtmánek:
Parallel Algorithms for Detection of Negative Cycles ,
2003. [bibtex, pdf]

Jiří Barnat, Luboš Brim, and Jakub Chaloupka:
Parallel Breadth-First Search LTL Model-Checking,
18th IEEE International Conference on Automated Software Engineering (ASE’03), IEEE Computer Society, 2003, 106–115. [bibtex]

Luboš Brim and Jitka Žídková:
Using Assumptions to Distribute Alternation Free mu-Calculus Model Checking,
2st International Workshop on Parallel and Distributed Model Checking (PDMC 2003), Elsevier, 2003, 19-34. [bibtex, url]

2002

Jiří Barnat, Luboš Brim, and Ivana Černá:
Property Driven Distribution of Nested DFS,
Proceeding of the 3rd International Workshop on Verification and Computational Logic (VCL’2002), 2002, 1–10. [bibtex]

Jiří Barnat, Luboš Brim, and Ivana Černá:
Property driven distribution of Nested DFS,
Proc. Workshop on Verification and Computational Logic, 2002, 1–10. [bibtex]

Luboš Brim, Jitka Crhová, and Karen Yorav:
Using Assumptions to Distribute CTL Model Checking,
1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), Elsevier, 2002, 80-95. [bibtex]

2001

Luboš Brim, Ivana Černá, Pavel Krčál, and Radek Pelánek:
Distributed LTL Model Checking Based on Negative Cycle Detection,
FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference, Bangalore, India, December 13-15, 2001, Proceedings, Springer Verlag, 2001, 96–107. [bibtex]

Jiří Barnat, Luboš Brim, and Jitka Stříbrná:
Distributed LTL Model-Checking in SPIN,
Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume 2057 of LNCS, 200–216. [bibtex]

Luboš Brim, Ivana Černá, Pavel Krčál, and Radek Pelánek:
Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths ,
2001. [bibtex, pdf]

Luboš Brim, Ivana Černá, Pavel Krčál, and Radek Pelánek:
How to Employ Reverse Search in Distributed Single-Source Shortest Paths ,
2001. [bibtex, pdf]

Luboš Brim, Ivana Černá, Pavel Krčál, and Radek Pelánek:
How to Employ Reverse Search in Distributed Single-Source Shortest Paths,
SOFSEM’01, Springer Verlag, 2001, 191–200. [bibtex]

Luboš Brim, Ivana Černá, and Martin Nečesal:
Randomization Helps in LTL Model Checking.,
Process Algebra and Probabilistic Methods. Performance Modelling and Verification (PAPM-PROBMIV), Springer, 2001, 105–119. [bibtex]