Publications

2017

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill:
Model Checking of C and C++ with DIVINE 4,
International Symposium on Automated Technology for Verification and Analysis (ATVA) (to appear), 2017, volume 10482 of Lecture Notes in Computer Science. [bibtex, pdf, url, paper page]

Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, and Jiří Barnat:
Optimizing and Caching SMT Queries in SymDIVINE,
Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, Springer Berlin Heidelberg, 2017, 390–393. [bibtex, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification,
IEEE International Conference on Software Quality, Reliability and Security (QRS), 2017, 54-64. [bibtex, pdf, url, paper page]

2016

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories,
Software Quality Journal, 2016. [bibtex, url]

Jaroslav Bendík:
Algorithms for Finding Maximal Satisfiable Sets of Constraints,
Master’s Thesis, 2016. [bibtex, pdf, url]

Jan Mrázek:
Caching SMT Queries in SymDIVINE,
Bachelor’s Thesis, 2016. [bibtex, pdf, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
DIVINE: Explicit-State LTL Model Checker,
Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2016, 920–922. [bibtex, pdf, url]

Jaroslav Bendík, Nikola Beneš, Jiří Barnat, and Ivana Černá:
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis,
Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings, 2016, 121–136. [bibtex, url]

Vladimír Štill:
LLVM Transformations for Model Checking,
Master’s Thesis, 2016. [bibtex, pdf, url]

Peter Bezděk, Nikola Beneš, Jiří Barnat, and Ivana Černá:
LTL Parameter Synthesis of Parametric Timed Automata,
Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings, 2016, 172–187. [bibtex, url]

Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, and Kristína Zákopčanová:
On Verifying C++ Programs with Probabilities,
ACM Symposium on Applied Computing, 2016, 1238–1243. [bibtex, url]

Eva Tesařová:
Optimal Sensor Scheduling for Systems under Temporal Constraints,
Master’s Thesis, 2016. [bibtex, pdf, url]

Jan Mrázek, Petr Bauch, Henrich Lauko, and Jiří Barnat:
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration,
Model Checking Software: 23rd International Symposium, SPIN, Springer International Publishing, 2016, 208–213. [bibtex, pdf, url]

Jiří Weiser:
TCP vrstva pro verifikační nástroj DIVINE,
Diplomová práce, 2016. [bibtex, pdf, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations,
Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture Notes in Computer Science, 144–155. [bibtex, pdf, url]

2015

Mária Svoreňová:
Control Strategy Synthesis for Path Planning under Temporal Constraints,
Ph.D. Thesis, 2015. [bibtex, pdf, url]

Jiří Barnat, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
Fast, Dynamically-Sized Concurrent Hash Table,
Model Checking Software (SPIN 2015), Springer International Publishing, 2015, volume 9232 of Lecture Notes in Computer Science, 49-65. [bibtex, pdf, url]

Petr Ročkai:
Model Checking Software,
Ph.D. Thesis, 2015. [bibtex, pdf, url]

Kristína Zákopčanová:
On Chaining Divine and Prism Model Checkers,
Bachelor’s Thesis, 2015. [bibtex, pdf, url]

Mária Svoreňová, Ivana Černá, and Calin Belta:
Optimal Temporal Logic Control for Deterministic Transition Systems with Probabilistic Penalties,
IEEE Transactions on Automatic Control, 2015. [bibtex]

Jiří Barnat:
Quo Vadis Explicit-State Model Checking,
SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, Springer, 2015, 46-57. [bibtex, url]

Petr Ročkai, Vladimír Štill, and Jiří Barnat:
Techniques for Memory-Efficient Model Checking of C and C++ Code,
Software Engineering and Formal Methods, Springer International Publishing, 2015, volume 9276 of Lecture Notes in Computer Science, 268–282. [bibtex, pdf, url]

Mária Svoreňová, Jan Křetínský, Martin Chmelík, Krishnendu Chatterjee, Ivana Černá, and Calin Belta:
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games,
Proceedings of ACM international conference on Hybrid Systems: Computation and Control, Association for Computing Machinery (ACM), 2015, 259-268. [bibtex]

Mária Svoreňová, Martin Chmelík, Kevin Leahy, Hasan Ferit Eniser, Krishnendu Chatterjee, Ivana Černá, and Calin Belta:
Temporal Logic Motion Planning using POMDPs with Parity Objectives,
Proceedings of ACM international conference on Hybrid Systems: Computation and Control, Association for Computing Machinery (ACM), 2015, 233-238. [bibtex]

Milan Lenčo:
Verification of Name Service Cache Daemon with DIVINE Model Checker,
Master’s Thesis, 2015. [bibtex, pdf, url]

2014

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Context-Switch-Directed Verification in DIVINE,
Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146. [bibtex, pdf, url]

Jaroslav Bendík:
Detekce cyklů v dynamických grafech,
Bakalářská práce, 2014. [bibtex, pdf, url]

Vojtěch Havel:
Generic Platform for Explicit-Symbolic Verification,
Master’s Thesis, 2014. [bibtex, pdf, url]

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
LTL Model Checking of LLVM Bitcode with Symbolic Data,
Proceedings of MEMICS’14, Springer, 2014, 47-59. [bibtex, url]

Peter Bezděk, Nikola Beneš, Jiří Barnat, and Ivana Černá:
LTL Model Checking of Parametric Timed Automata,
MEMICS 2014, NOVPRESS, 2014, 28-39. [bibtex]

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

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Model Checking Parallel Programs with Inputs,
Parallel, Distributed and Network-Based Processing (PDP), 2014 22nd Euromicro International Conference on, 2014, 756-759. [bibtex, url]

Eva Tesařová:
Modelování systémů s reálným časem a pravděpodobností,
Bakalářská práce, 2014. [bibtex, pdf, url]

Peter Bezděk, Nikola Beneš, Vojtěch Havel, Jiří Barnat, and Ivana Černá:
On Clock-Aware LTL properties of Timed Automata,
International Colloquium on Theoretical Aspects of Computing (ICTAC), Springer, 2014, volume 8687 of LNCS, 46–60. [bibtex]

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Temporal Verification of Simulink Diagrams,
Proceedings of HASE 2014, IEEE Computer Society, 2014, 81-88. [bibtex]

Jiří Barnat, Nikola Beneš, Tomáš Bureš, Ivana Černá, Jaroslav Keznikl, and František Plášil:
Towards Verification of Ensemble-Based Component Systems,
Formal Aspects of Component Software (FACS), Springer, 2014, volume 8348 of LNCS, 1–20. [bibtex]

2013

Jiří Barnat, Nikola Beneš, Ivana Černá, and Zuzana Petruchová:
DCCL: Verification of Component Systems with Ensembles,
Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, ACM, 2013, 43–52. [bibtex, url]

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]

Jiří Barnat, Jan Havlíček, and Petr Ročkai:
Distributed LTL Model Checking with Hash Compaction,
Electronic Notes in Theoretical Computer Science, Volume 296, Elsevier Science, 2013, 79-93. [bibtex, url]

Jiří Weiser:
Dynamicky rostoucí sdílená hašovací tabulka pro DiVinE,
Bakalářská práce, 2013. [bibtex, pdf, 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]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Formal analysis of piecewise affine systems through formula-guided refinement,
Automatica, 2013, 261–266. [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]

Mária Svoreňová, Ivana Černá, and Calin Belta:
Optimal Control of MDPs with Temporal Logic Constraints,
Proceedings of The 52nd IEEE Conference on Decision and Control, Omnipress for the IEEE Control Systems Society, 2013, 3938-3943. [bibtex, url]

Mária Svoreňová, Ivana Černá, and Calin Belta:
Optimal Receding Horizon Control for Finite Deterministic Systems with Temporal Logic Constraints,
Proceedings of The 2013 American Control Conference, Institute of Electrical and Electronics Engineers ( IEEE ), 2013, 4399 - 4404. [bibtex, url]

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]

Vladimír Štill:
State Space Compression for the DiVinE Model Checker,
Bachelor’s Thesis, 2013. [bibtex, pdf, 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]

Jan Havlíček:
Untimed LTL Model Checking of Timed Automata,
Master’s Thesis, 2013. [bibtex, pdf, url]

2012

Mária Svoreňová, Jana Tůmová, Jiří Barnat, and Ivana Černá:
Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints,
IEEE Conference on Decision and Control (CDC 2012), Omnipress for IEEE Control Systems Society, 2012, 6749–6754. [bibtex]

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]

Nikola Beneš, Ivana Černá, and Filip Štefaňák:
Factorization for Component-Interaction Automata,
SOFSEM 2012: Theory and Practice of Computer Science, Springer Berlin Heidelberg, 2012, volume 7147 of Lecture Notes in Computer Science, 554-565. [bibtex, url]

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]

Vojtěch Havel:
Relaxed Memory Models in DiVinE,
Bachelor’s Thesis, 2012. [bibtex, pdf, url]

Nikola Beneš, Barbora Bühnová, Ivana Černá, and Radek Ošlejšek:
Reliability analysis in component-based development via probabilistic model checking,
Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering (CBSE ’12), ACM, 2012, 83-92. [bibtex, url]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems,
IEEE Transactions on Automatic Control, 2012. [bibtex, url]

Boyan Yordanov, Jana Tůmová, Ivana Černá, Jiří Barnat, and Calin Belta:
Temporal Logic Control of Discrete-Time Piecewise Affine Systems,
IEEE Transactions on Automatic Control, 2012. [bibtex, url]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Timed Automata Approach to Verification of Systems with Degradation,
MEMICS 2011, Springer, 2012, 84 - 93. [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]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Verification of Systems with Degradation,
Computing and Informatics, 2012. [bibtex]

2011

Pieter Collins, Luc Habets, Jan van Schuppen, Ivana Černá, Jana Fabriková, and David Šafránek:
Abstraction of Biochemical Reaction Systems on Polytopes,
Proceedings of the 18th IFAC World Congress, IFAC, 2011, 14869-14875. [bibtex, url]

Nikola Beneš, Ivana Černá, and Milan Křivánek:
CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems,
Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, Open Publishing Association, 2011, 63-67. [bibtex, url]

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]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, 2011. [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š, Ivana Černá, and Jan Křetínský:
Modal Transition Systems: Composition and LTL Model Checking,
ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium, Springer, 2011, 228-242. [bibtex]

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]

Roman Plášil:
Vysvětlování protipříkladů v nástroji DiVinE [online],
Master’s Thesis, 2011. [bibtex, url]

2010

Jana Tůmová, Boyan Yordanov, Calin Belta, Ivana Černá, and Jiří Barnat:
A Symbolic Approach to Controlling Piecewise Affine Systems,
Proceedings of of the 49th IEEE Conference on Decision and Control (CDC), Omnipress for IEEE Control Systems Society, 2010, 4230 -4235. [bibtex]

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, Jakub Chaloupka, and Jaco van de Pol:
Distributed Algorithms for SCC Decomposition,
Journal of Logic and Computation, 2010. [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]

Boyan Yordanov, Jana Tůmová, Calin Belta, Ivana Černá, and Jiří Barnat:
Formal Analysis of Piecewise Affine Systems through Formula -Guided Refinement,
Proceedings of of the 49th IEEE Conference on Decision and Control (CDC), Omnipress for IEEE Control Systems Society, 2010, 5899 -5904. [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]

Petr Ročkai:
Partial Order Reduction in Parallel Model Checking,
Master’s Thesis, 2010. [bibtex, pdf, url]

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]

Mária Svoreňová:
Verifikace hybridních systémů,
Bakalářská práce, 2010. [bibtex, pdf, 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]

Radek Pelánek:
Fighting State Space Explosion: Review and Evaluation,
Formal Methods for Industrial Critical Systems: 13th International Workshop, FMICS 2008, L’Aquila, Italy, September 15-16, 2008, Revised Selected Papers, Springer Berlin Heidelberg, 2009, 37–52. [bibtex, url]

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]

Laura Bozzelli, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček:
On Decidability of LTL Model Checking for Process Rewrite Systems,
Acta informatica, 2009. [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]

Jiří Barnat, Ivana Černá, and Jana Tůmová:
Quantitative Model Checking of Systems with Degradation,
Proceeding of the Sixth International Conference on Quantitative Evaluation of Systems (QEST 2009), IEEE, 2009, 21–30. [bibtex]

2008

Nikola Beneš, Ivana Černá, Jiří Sochor, Pavlína Vařeková, and Barbora Zimmerová:
A Case Study in Parallel Verification of Component-Based Systems,
Electr. Notes Theor. Comput. Sci., 2008, 67–83. [bibtex, url]

Pavlína Vařeková and Ivana Černá:
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems,
Proceedings of FACS’08, 2008, 41–55. [bibtex]

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]

Pavlína Vařeková, Barbora Zimmerová, Pavel Moravec, and Ivana Černá:
Formal Verification of Systems with an Unlimited Number of Components,
IET Software journal, Institution of Engineering and Technology (IET), 2008, 532–546. [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, Jakub Chaloupka, and Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition,
ENTCS, 2008, 63–77. [bibtex]

Jiří Barnat, Jakub Chaloupka, and Jaco van de Pol:
Improved Distributed Algorithms for SCC Decomposition,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers B. V., 2008, 63–77. [bibtex, url]

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]

Pavlína Vařeková and Ivana Černá:
Model Checking of Control-User Component-Based Parametrised Systems,
CBSE’08, Springer, 2008, volume 5282 of Lecture Notes in Computer Science, 146–162. [bibtex]

Radek Pelánek:
Model Classifications and Automated Verification,
Formal Methods for Industrial Critical Systems: 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers, Springer Berlin Heidelberg, 2008, 149–163. [bibtex, url]

Petr Ročkai:
Multi-Threaded Nested DFS,
Bachelor’s Thesis, 2008. [bibtex, pdf, url]

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]

Stefan Edelkamp, Peter Sanders, and Pavel Šimeček:
Semi-external LTL Model Checking,
20th International Conference on Computer Aided Verification, Springer, 2008, 530-542. [bibtex]

Jiří Barnat and Petr Ročkai:
Shared Hash Tables in Parallel Model Checking,
ENTCS, 2008, 79–91. [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

Radek Pelánek:
BEEM: Benchmarks for Explicit Model Checkers,
Model Checking Software, Springer Berlin Heidelberg, 2007, volume 4595 of Lecture Notes in Computer Science, 263–267. [bibtex, url]

Pavelína Vařeková and Barbora Zimmerová:
Challenge Problem: Subject-Observer Specification with Component-Interaction Automata,
Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007, 75–81. [bibtex]

Ivana Černá, Pavlína Vařeková, and Barbora Zimmerová:
Component Substitutability via Equivalencies of Component-Interaction Automata,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2007, 39–55. [bibtex, url]

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]

Pavlína Vařeková, Pavel Moravec, Ivana Černá, and Barbora Zimmerová:
Effective Verification of Systems with a Dynamic Number of Components,
Proceedings of the ESEC/FSE Conference on Specification and Verification of Component-Based Systems (SAVCBS’07), ACM Press, 2007, 3–13. [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]

Ahmed Bouajjani, Jan Strejček, and Tayssir Touili:
On Symbolic Verification of Weakly Extended PAD,
Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006), Elsevier, 2007, 47-64. [bibtex, url]

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]

Ivana Černá, Pavlína Vařeková, and Barbora Zimmerová:
Component Substitutability via Equivalencies of Component-Interaction Automata,
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS’06), UNU-IIST, 2006, 115-130. [bibtex]

Radek Pelánek and Jan Strejček:
Deeper Connections Between LTL and Alternating Automata,
Implementation and Application of Automata: 10th International Conference, CIAA 2005, Sophia Antipolis, France, June 27-29, 2005, Revised Selected Papers, Springer Berlin Heidelberg, 2006, 238–249. [bibtex, url]

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]

Jiří Barnat and Ivana Černá:
Distributed Breadth-First Search LTL Model Checking,
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, 2006, 117–134(18). [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]

Ivana Černá and Tomáš Brázdil:
Model Checking of RegCTL,
Computing and Informatics, 2006. [bibtex]

Jiří Šimša:
Monitorování chování systémů,
Master’s Thesis, 2006. [bibtex, pdf, url]

Laura Bozzelli, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček:
On Decidability of LTL Model Checking for Process Rewrite Systems,
FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, Springer-Verlag, 2006, 248-259. [bibtex]

Jiří Barnat and Pavel Moravec:
Parallel Algorithms for Finding SCCs in Implicitly Given Graphs,
Formal Methods: Applications and Technology, Springer, 2006, volume 4346 of LNCS, 316–330. [bibtex]

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]

Jiří Barnat, Vojěch Forejt, Martin Leucker, and Michael Weber:
DivSPIN – A SPIN compatible distributed model checker,
Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, 2005, 95–100. [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]

Pavel Moravec:
How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking,
1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005), FI MU Report Series, 2005, 186-192. [bibtex, url]

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]

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček:
Reachability Analysis of Multithreaded Software with Asynchronous Communication,
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science: 25th International Conference, Hyderabad, India, December 15-18, 2005. Proceedings, Springer Berlin Heidelberg, 2005, 348–359. [bibtex, url]

Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček:
Reachability of Hennessy - Milner properties for weakly extended PRS,
FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Springer-Verlag, 2005, 213-224. [bibtex]

Antonín Kučera and Jan Strejček:
The stuttering principle revisited,
Acta informatica, 2005. [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]

Tomáš Brázdil, Antonín Kučera, and Oldřich Stražovský:
Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems,
Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), Springer, 2004, 193-208. [bibtex]

Jiří Barnat:
Distributed Memory LTL Model Checking,
2004. [bibtex]

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]

Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček:
Extended Process Rewrite Systems: Expressiveness and Reachability,
CONCUR 2004 - Concurrency Theory, Springer, 2004, 355-370. [bibtex]

David Antoš, Vojtěch Řehák, and Jan Kořenek:
Hardware Router’s Lookup Machine and its Formal Verification,
ICN’2004 Conference Proceedings, University of Haute Alsace, Colmar, France, 2004, 1002-1007. [bibtex, url]

Jan Strejček:
Linear Temporal Logic: Expressiveness and Model Checking,
2004. [bibtex, pdf]

Gerd Behrmann, Patricia Bouyer, Kim G. Larsen, and Peláne Radek:
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata,
Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings, Springer Berlin Heidelberg, 2004, 312–326. [bibtex, url]

Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček:
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit,
INFINITY’2003: 5th International Workshop on Verification of Infinite-State Systems, Elsevier Science, 2004, 75-88. [bibtex, url]

Vojtěch Řehák:
Reachability for Extended Process Rewrite Systems,
MOVEP’04: 6th school on MOdeling and VErifying parallel Processes, Universite Libre de Bruxelles, 2004, 77-82. [bibtex]

Radek Pelánek:
Typical Structural Properties of State Spaces,
Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004. Proceedings, Springer Berlin Heidelberg, 2004, 5–22. [bibtex, url]

David Šafránek:
Visual Coordination Diagrams,
Proceedings of the Doctoral Symposium of 7th International Conference on the Unified Modeling Language, Alanen M., Cabot J., Goulao M., Saez J. and Simmonds D. (editors), 2004, 53-60. [bibtex, url]

David Šafránek:
Visual Specification of Systems with Heterogeneous Coordination Models,
Proceeding of 3rd International Workshop on Foundations of Coordination Languages and Software Architectures, ENTCS, 2004, 107-121. [bibtex]

2003

Ivana Černá and Radek Pelánek:
Distributed Explicit Fair Cycle Detection (Set Based Approach),
Model Checking Software. 10th International SPIN Workshop, Springer Verlag, 2003, volume 2648 of Lecture Notes in Computer Science, 49 – 73. [bibtex, pdf]

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]

Radek Pelánek:
LTL Hierarchies and Model Checking,
Proceedings of the Eight ESSLLI Student Session, TU Wien, 2003, 245-254. [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]

Ivana Černá and Radek Pelánek:
Relating Hierarchy of Temporal Properties to Model Checking,
Mathematical Foundations of Computer Science (MFCS), Springer, 2003, volume 2747 of LNCS, 318 - 327. [bibtex]

Ivana Černá and Radek Pelánek:
Relating Hierarchy of Temporal Properties to Model Checking,
2003. [bibtex, pdf]

Gerd Behrmann, Kim G. Larsen, and Radek Pelánek:
To Store or Not To Store,
Computer Aided Verification (CAV 2003), Springer-Verlag, 2003, 433-445. [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]

David Šafránek:
Visual specification of concurrent systems,
Automated Software Engineering, 2003. Proceedings. 18th IEEE International Conference on, 2003, 369-372. [bibtex, url]

David Antoš, Jan Kořenek, and Vojtěch Řehák:
Vyhledávání v IPv6 směrovači implementovaném v hradlovém poli,
EurOpen, Sborník příspěvků XXIII. konference, EurOpen, 2003, 91-102. [bibtex]

2002

Vojtěch Řehák:
$\xor$-OBDD in Symbolic Model Checking,
SOFSEM 2002: Student Research Forum, Slovak University of Technology, 2002, 41-46. [bibtex]

Jan Strejček:
Boundaries and Efficiency of Verification,
Proceedings of summer school MOVEP~2002, IRCCyN, Ecole Centrale de Nantes, France, 2002, 403-408. [bibtex]

Ivana Černá and Radek Pelánek:
Distributed Explicit Fair cycle Detection,
2002. [bibtex, pdf]

Jiří Barnat:
How to Distribute LTL Model-checking Using Decomposition of Negative Claim Automaton,
SOFSEM 2002 Student Research Forum, 2002, 9–14. [bibtex]

Tomáš Brázdil and Ivana Černá:
Local Distributed Model Checking of RegCTL,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002. [bibtex]

Jiří Barnat, Tomáš Brázdil, Pavel Krčál, Vojtěch Řehák, and David Šafránek:
Model Checking in IPv6 Hardware Router Design,
2002, 8. [bibtex]

Jitka Stříbrná and Ivana Černá:
Modifications of Expansion Trees for Weak Bisimulation in BPA,
Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002. [bibtex]

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]

David Šafránek:
SGCCS: A Graphical Language for Real-Time Coordination,
Proceedings of 1th International Workshop on Foundations of Coordination Languages and Software Architectures, Elsevier Science, 2002, 99-114. [bibtex, url]

David Šafránek:
SGCCS: A Graphical Language for Real-Time Systems,
Proceedings SOFSEM 2002 Student Research Forum, Mária Bieliková, 2002, 47-52. [bibtex, url]

Antonín Kučera and Jan Strejček:
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL,
Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL’02), Springer, 2002, 276-291. [bibtex]

Antonín Kučera and Jan Strejček:
The Stuttering Principle Revisited: On the Expressiveness of Nested X and ⋃ Operators in the Logic LTL,
Computer Science Logic: 16th International Workshop, CSL 2002 11th Annual Conference of the EACSL Edinburgh, Scotland, UK, September 22–25, 2002 Proceedings, Springer Berlin Heidelberg, 2002, 276–291. [bibtex, url]

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]

Jitka Crhová, Pavel Krčál, Jan Strejček, David Šafránek, and Pavel Šimeček:
YAHODA: verification tools database,
Proceedings of Tools Day, FI MU, 2002, 99-103. [bibtex, url]

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]

Jan Strejček:
Models of Infinite-State Systems with Constraints,
Master’s Thesis, 2001. [bibtex, pdf, url]

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]

Jan Strejček:
Rewrite Systems with Constraints,
EXPRESS’01 the 8th International Workshop on Expressiveness in Concurrency, Elsevier Science, 2001, 1-20. [bibtex, url]

2000

Jan Strejček:
Constrained Rewrite Transition Systems,
FI MU, 2000. [bibtex, pdf, url]

Ivana Černá and Jitka Stříbrná:
Some Remarks on Weak Bisimilarity of BPA-Processes,
2000. [bibtex, pdf]

1999

Ivana Černá, Mojmír Křetínský, and Antonín Kučera:
Comparing Expressibility of Normed BPA and BPP Processes,
Acta Informatica, 1999, 233 - 256. [bibtex]

Ivana Černá, Ondřej Klíma, and Jiří Srba:
On the Pattern Equations ,
1999. [bibtex, pdf]

Ivana Černá, Ondřej Klíma, and Jiří Srba:
Pattern Equations and Equations with Stuttering,
SOFSEM’99, Springer, 1999, 369–378. [bibtex]

1996

Ivana Černá, Mojmír Křetínský, and Antonín Kučera:
Bisimilarity is Decidable in the Union of Normed BPA and BPP Processes,
Proceedings of the 1st International Workshop on Verification of Infinite State Systems , 1996, 32 -46. [bibtex]

Ivana Černá, Mojmír Křetínský, and Antonín Kučera:
Comparing Expressibility of Normed BPA and BPP Processes,
1996. [bibtex, pdf]

Ivana Černá, Mojmír Křetínský, and Antonín Kučera:
On the Relationship between Sequential and Parallel Compositions in Process Algebras,
CSL96 - The 1996 Annual Conference of the European Assoc.., Department of Philosophy, Ulterech University, 1996, 11-13. [bibtex]

Ivana Štefáneková:
Some properties of zerotesting bounded one-way multicounter machines,
1996. [bibtex]

1991

Andrej Bebják and Ivana Štefáneková:
Separation of deterministic, nondeterministic and alternating complexity classes,
Theoretical Computer Science, 1991, 297 - 311. [bibtex]

1990

Ivana Štefáneková:
Some properties of zerotesting bounded one-way multicounter machines,
Proceedings of Mathematical Foundations of Computer Science, Springer Verlag, 1990, volume 452 of Lecture Notes in Computer Science, 195 - 201. [bibtex]

1989

Dana Pardubská and Ivana Štefáneková:
Nondeterministic multicounter machines and complementation,
Theoretical Computer Science, 1989, 111 - 113. [bibtex]

1988

Andrej Bebják and Ivana Štefáneková:
Nondeterminism is essential for reversal-bounded two-way multihead finite automata,
Kybernetika, 1988, 65 - 71. [bibtex]

Andrej Bebják and Ivana Štefáneková:
Relation between one-time-only braching programs and real-time branching programs,
Computers and Artificial Intelligence, 1988, 107 - 111. [bibtex]