My main interest is in formal verification as a framework for modelling, analyzing, verifying, and synthesizing complex systems. The main topic is currently distributed model checking of temporal properties.
Journals
 On clockaware LTL parameter
synthesis of timed automata
by P. Bezdek, N. Benes, I. Cerna and J. Barnat
J. Log. Algebr. Meth. Program vol. 99, pp. 114142, 2018. Bibtex  DiVM: Model checking with {LLVM} and graph memory
by P. Rockai, V. Still, I. Cerna, J. Barnat
Journal of Systems and Software vol. 143, pp. 1  13, 2018. Bibtex  Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
by M. Svorenova, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cerna, C. Belta
Nonlinear Analysis: Hybrid Systems vol. 23, pp. 230253, 2017. Bibtex  Optimal
Temporal Logic Control for Deterministic Transition Systems with
Probabilistic Penalties
by M. Svorenova, I. Cerna and C. Belta
IEEE Transactions on Automatic Control vol. 60, no. 6, pp. 114, 2015. Bibtex  Optimal
Temporal Logic Control for Deterministic Transition Systems with
Probabilistic Penalties
by M. Svorenova, I. Cerna and C. Belta
IEEE Transactions on Automatic Control vol. 60, no. 6, pp. 114, 2015. Bibtex 
Formal analysis of piecewise affine systems through formulaguided refinement.
by B. Yordanov, J. Tumova, I. Cerna, J. Barnat, C. Belta
In Automatica, volume 49(1), pp. 261266, 2013 Bibtex  Temporal
Logic Control of DiscreteTime Piecewise Affine Systems.
by B. Yordanov, J. Tumova, I. Cerna, J. Barnat, C. Belta
In IEEE Transactions on Automatic Control, vol. 57, no. 6, pp. 14911504, 2012. Bibtex  Verification of Systems with Degradation
by J. Barnat, I. Cerna, J. Tumova
In Computing and Informatics, vol. 31, pp. 507530, 2012. Bibtex 
Partial Order Reduction for State/Event LTL with Application to
ComponentInteraction Automata
by N. Benes, L. Brim, B. Buhnova, I. Cerna, J. Sochor, P. Moravcova Varekova
In Science of Computer Programming, Elsevier, vol. 76, no. 10, pp. 877890, 2011. Bibtex  On
Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking
by J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek
In Theoretical Computer Science. ISSN 03043975, 2009, vol. 2009, no. 410, s. 31283148. Bibtex  Formal
Verification of Systems with an Unlimited Number of Components
by P. Varekova, B. Zimmerova, P. Moravec, I. Cerna
In IET Software journal, volume 2(6), December 2008, 532546. Bibtex  Model
checking of RegCTL.
by T. Brazdil and I. Cerna
In Computing and Informatics, 2006, vol. 25, n. 1, p. 8197. Bibtex  Comparing Expressibility of Normed BPA and
Normed BPP Processes.
by I. Cerna, M. Kretinsky, and A. Kucera.
Acta Informatica, 36(3):233256. Springer, 1999 Bibtex 
Distributed BreadthFirst Search LTL Model Checking.
by J. Barnat and I. Cerna
Special Issue on Parallel and Distributed Databases of Formal Methods in System Design, volume 29(2), September 2006, 117134(18). Bibtex
 Separation of deterministic, nondeterministic and
alternating complexity classes.
by A. Bebjak, I. Stefanekova
Theoretical Computer Science, 88:297311, 1991 Bibtex  Nondeterministic multicounter machines and
complementation.
by D. Pardubska, I. Stefanekova
Theoretical Computer Science,67:111113, 1989. Bibtex  Relation between onetimeonly branching programs and
realtime branching programs.
by A. Bebjak, I. Stefanekova
Computers and Artificial Intelligence, 7:107111, 1988 Bibtex  Nondeterminism is essential for
reversalbounded
twoway multihead automata.
by A. Bebjak, I. Stefanekova
Kybernetika,24:6571, 1988. Bibtex
Proceedings

Online Enumeration of All Minimal Inductive Validity Cores
by J. Bendik, E. Ghassabani, M. Whalen, I. Cerna.
In Proceedings of the 16th International Conference Software Engineering and Formal Methods (SEFM), pp. 189204, 2018. Bibtex  Optimal observation mode
scheduling for systems under temporal constraints.
by E.Tesarova, M. Svorenova, J. Barnat, I. Cerna.
In Proceedings of the 2016 American Control Conference (ACC), pp. 10991104, 2016. Bibtex  Tunable Online MUS/MSS Enumerations.
by J. Bendik, N. Benes, I. Cerna, J. Barnat.
In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016), vol. 65, pp. 50:150:13, Schloss DagstuhlLeibnizZentrum fuer Informatik, 2016. Bibtex  LTL Parameter Synthesis of Parametric Timed Automata.
by P. Bezdek, N. Benes, J. Barnat, I. Cerna.
In Proceedings of the 14th International Conference Software Engineering and Formal Methods (SEFM), Vienna, pp. 172187. 2016. Bibtex  Finding
Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis.
by J. Bendik, N. Benes, J. Barnat, I. Cerna.
In Proceedings of the 14th International Conference Software Engineering and Formal Methods (SEFM), Vienna, pp. 121136. 2016. Bibtex  On verifying {C++}
programs with probabilities.
by J. Barnat, I. Cerna, P. Rockai, V. Still, K. Zakopcanova.
In Proceedings of the 31st Annual {ACM} Symposium on Applied Computing, Pisa, pp. 12381243. 2016. Bibtex  Temporal Logic Control for
Stochastic Linear
Systems using Abstraction Refinement of Probabilistic Games.
by M. Svorenova, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cerna, C. Belta.
In Proceedings of ACM international conference on Hybrid Systems: Computation and Control. Seattle, Washington, USA : Association for Computing Machinery (ACM), pp. 259268. 2015. Bibtex  Temporal Logic
Motion Planning using POMDPs with Parity Objectives.
by M. Svorenova, M. Chmelik, K. Leahy, H. F. Eniser, K. Chatterjee, I. Cerna, C. Belta.
In Proceedings of ACM international conference on Hybrid Systems: Computation and Control. Seattle, Washington, USA : Association for Computing Machinery (ACM), pp. 259268. 2015. Bibtex  LTL Model Checking of Parametric Timed
Automata.
by P. Bezdek, N. Benes, J. Barbat, I. Cerna
In Proceedings of MEMICS 2014. Brno, Czech Republic: NOVPRESS, 2014. p. 2839. Bibtex  On
ClockAware LTL properties of Timed Automata.
by P. Bezdek, N. Benes, V. Havel, J. Barbat, I. Cerna
In Proceedings of Theoretical Aspects of Computing (ICTAC) 2014. Springer, 2014, volume 8687 of LNCS, 4660. Bibtex  Towards
Verification of EnsembleBased Component Systems,
by J. Barnat, N. Benes, T. Bures, I. Cerna, J. Keznikl, F. Plasil
In Proceedings of Formal Aspects of Component Software (FACS), Springer, 2014, volume 8348 of LNCS, 120. Bibtex  DCCL: Verification of Component Systems with
Ensembles,
by J. Barnat, N. Benes, I. Cerna, Z. Petruchova
In Proceedings of he 16th International ACM Sigsoft symposium on Componentbased software engineering, ACM, 2013, CBSE '13, 4352. Bibtex  Optimal
Control of MDPs with Temporal Logic Constraints
by M. Svorenova, I. Cerna, C. Belta
In Proceedings of IEEE Conference on Decision and Control (CDC), p. 39383943, 2013. Bibtex  Optimal
Receding Horizon Control for Finite Deterministic Systems with
Temporal Logic Constraints
by M. Svorenova, I. Cerna, C. Belta
In Proceedings of American Control Conference (ACC), p. 43994404, 2013. Bibtex 
Attractionbased receding horizon path planning with temporal logic constraints.
by M. Svorenova, J. Tumova, I. Cerna, J. Barnat
In Proceedings of IEEE Conference on Decision and Control (CDC), p. 67496754, 2012. Bibtex 
Factorization for ComponentInteraction Automata
by N. Benes, I. Cerna, F. Stefanak
In Proceedings of SOFSEM 2012: Theory and Practice of Computer Science. LNCS 7147, pp. 554565, 2012. Bibtex  Reliability Analysis
in Componentbased Development via Probabilistic Model Checking
by N. Benes, B. Buhnova, I. Cerna, R. Oslejsek
In Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering (CBSE '12). ACM , pp. 8392, 2012. Bibtex  Timed
Automata Approach to Verification of Systems with Degradation
by J. Barnat, J. Tumova, I. Cerna
In Proceedings of MEMICS 2011, LNCS 7119, Springer, pp. 84  93. 2012. Bibtex  Abstraction of Biochemical Reaction Systems on
Polytopes
by P. Collins, P. Habets, J. van Schuppen, I. Cerna, J. Fabrikova, D. Safranek
In Proceedings of the 18th IFAC World Congress. Milano : IFAC, 2011. pp. 1486914875, 2011. Bibtex  CoInDiVinE: Parallel Distributed Model
Checker for ComponentBased Systems
by N. Benes, I. Cerna, M. Krivanek
In Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation. Open Publishing Association, 2011. pp. 6367. 2011, Snowbird, Utah, USA. Bibtex  Modal
Transition Systems: Composition and LTL Model Checking
by N. Benes, I. Cerna, J. Kretinsky
In Proceedings of ATVA 2011  Automated Technology for Verification and Analysis: 9th International Symposium. Springer, LNCS 6996, pp. 228242, 2011. Bibtex  A
Symbolic Approach to Controlling Piecewise Affine Systems
by J. Tumova, B. Yordanov, C. Belta, I. Cerna, J. Barnat
In Proceedings of IEEE Conference on Decision and Control (CDC), pp. 42304235, 2010. Bibtex  Formal
Analysis of Piecewise Affine Systems through FormulaGuided Refinement
by B. Yordanov, J. Tumova, C. Belta, I. Cerna, J. Barnat
In Proceedings of IEEE Conference on Decision and Control (CDC), pp. 58995904, 2010. Bibtex  BioDiVinE: A Framework for Parallel
Analysis of Biological Models
by J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, J. Lanik, D. Safranek, Hongwu Ma
In Electronic Proceedings in Theoretical Computer Science (COMPMOD 2009), volume 6, 2009, 3145. Bibtex  BioDiVinE: A Tool for Parallel Analysis of
MultiAffine ODE Models,
by J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, J. Lanik, D. Safranek
In Proceedings of The 7th Conference on Computational Methods in Systems Biology (CMSB'09), Universita di Pisa, 2009, volume TR0909 of Technical Report, 15. Bibtex  Computational Analysis of LargeScale
MultiAffine ODE Models,
by J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, D. Safranek
In Proceedings of International Workshop on High Performance Computational Systems Biology (HiBi 2009), IEEE Computer Society Press, 2009, 8190. Bibtex  Partial
Order Reduction for State/Event LTL
by N. Benes, L. Brim, I. Cerna, J. Sochor, P. Varekova, B Zimmerova
In Proceedings of the International Conference on Integrated Formal Methods (IFM'09), SpringerVerlag, 2009, volume 5423 of LNCS, 307321. Bibtex 
Quantitative Model Checking of Systems with Degradation
by J. Barnat, I. Cerna, J. Tumova
In Proceedings of the Sixth International Conference on Quantitative Evaluation of Systems (QEST 2009), IEEE, 2009, 2130. Bibtex 
Local Quantitative LTL Model Checking
by J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova
In Proceedings of International Workshop on Formal Methods for Industrial Critical Systems (FMICS), pp. 5368, 2008. Bibtex 
Automated Computing of the Maximal Number of Handled Clients for ClientServer Systems
by P. Varekova, I. Varekova, I. Cerna
In Proceedings of Proceedings of FACS'08, 2008, 4155. Bibtex  Model
Checking of ControlUser ComponentBased Parametrised Systems
by P. Varekova, I. Cerna
In Proceedings of CBSE'08, Springer, 2008, volume 5282 of Lecture Notes in Computer Science, 146162. Bibtex 
Parallel Model Checking LargeScale Genetic Regulatory Networks with DiVinE
by J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek
In ENTCS, volume 194(3), 2008, 3550. Bibtex  ProbDiVinEMC: Multicore LTL Model Checker for
Probabilistic Systems
by J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova
In Proceedings of QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, IEEE Computer Society, 2008, 7778. Bibtex  A Case Study in Parallel Verification of
ComponentBased Systems
by N. Benes, J. Cerna, J. Sochor, P. Varekova, B. Zimmerova
In Electr. Notes Theor. Comput. Sci., volume 220(2), 2008, 6783. Bibtex  The CoIn Tool: Modelling and Verification of
Interactions in ComponentBased Systems
by N. Benes, L. Brim, I. Cerna, J. Sochor, P. Varekova, B. Zimmerova
In Proceedings of the Workshop on Formal Aspects of Component Software (FACS'08), 2008, 221225. Bibtex  ComponentInteraction Automata Approach (CoIn)
by B. Zimmerova, P. Varekova, N. Benes, I. Cerna, L. Brim, J. Sochor
In The Common Component Modeling Example: Comparing Software Component Models, Springer, LNCS 5153, pp. 146  176, 2008. Bibtex 
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional
Networks
by J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek
In Proceedings of PDMC 2008  Parallel and Distributed Methods ins VerifiCation. p. 8396, 2008. Bibtex 
Component Substitutability via Equivalencies of ComponentInteraction Automata
by I. Cerna, P. Varekova, B. Zimmerova
In Electronic Notes in Theoretical Computer Science, volume 182, June 2007, 3955. Bibtex 
Effective Verification of Systems with a Dynamic Number of Components
by P. Varekova, P. Moravec, I. Cerna, B. Zimmerova
In Proceedings of the ESEC/FSE Conference on Specification and Verification of ComponentBased Systems (SAVCBS'07), ACM Press, 2007, 313. Bibtex  On Combining Partial Order Reduction with
Fairness Assumptions
by L. Brim, I. Cerna, P. Moravec, J. Simsa
In Proceedings of FMICS/PDMC, 2007, volume 4346 of Lecture Notes in Computer Science, 84  99. Bibtex  ProbDiVinE: A Parallel Qualitative LTL Model Checker
by J. Barnat, L. Brim, I. Cerna, M. Ceska, J. Tumova
In Proceedings of Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07), IEEE Computer Society, 2007, 215216. Bibtex  ClusterBased LTL
Model Checking of Large Systems
by J. Barnat, L. Brim, I. Cerna
In Proceedings of Formal Methods for Components and Objects. Springer, LNCS 4111, 2006. p. 259279. Bibtex  Component Substitutability via Equivalencies of ComponentInteraction Automata
by I. Cerna, O. Varekova, B. Zimmerova
In Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06). Macao: UNUIIST, 2006. p. 115130. Bibtex  How to Order Vertices for Distributed
LTL ModelChecking Based
on Accepting Predecessors.
by L. Brim, I. Cerna, P.Moravec and J. Simsa
in 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05),
volume 135 of Electronic Notes in Theoretical Computer Science, issue 2, Elsevier Science Publishers, pages 318, 2006. Bibtex  DiVinE The Distributed Verification
Environment.
by J. Barnat, L. Brim, I. Cerna, and P. Simecek
in 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'05),
volume xxx of Electronic Notes in Theoretical Computer Science, issue x, Elsevier Science Publishers, 2006. Bibtex  Enhancing Random Walk State Space Exploration.
by R. Pelanek, T. Hanzl, I. Cerna and L. Brim
in Proceedings of Tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 05),Lisbon, Portugal.
ACM Press, pages 98  105, 2005. Bibtex 
ComponentInteraction Automata as a VerificationOriented
ComponentBased System Specification.
by B. Zimmerova, L. Brim, I. Cerna and P. Varekova
in Specification and Verification of ComponentBased Systems (SAVCBS 05),
pages 352  366, , 2005. Bibtex  Accepting Predecessors are Better than Back
Edges in Distributed LTL ModelChecking.
by L. Brim, I. Cerna, P. Moravec and J. Simsa
in Proc. Formal Methods in ComputerAided Design (FMCAD2004),
pages 352  366, volume 3312 of Lecture Notes of Computer Science, SpringerVerlag, 2005. Bibtex 
Distributed Partial Order Reduction of
State Spaces.
by L. Brim, I. Cerna, P.Moravec and J. Simsa
In Proceedings of 3rd International Workshop on Parallel and Distributed Methods in VerifiCation PDMC'2004.
volume 128 of Electronic Notes in Theoretical Computer Science, issue 3, Elsevier Science Publishers, 2005. Bibtex  Distributed Negative Cycle Detection Algorithms.
by L. Brim, I. Cerna and L. Hejtmanek
Parallel Computing: Software Technology, Algorithms, Architectures & Applications, Elsevier, 2004. Bibtex  Relating Hierarchy of Temporal Properties to
Model Checking.
by I. Cerna, R. Pelanek
in Proceedings of Mathematical Foundations of Computer Science MFCS'03
pages 318  327, volume 2747 of Lecture Notes of Computer Science, SpringerVerlag, 2003. Bibtex  Distributed Explicit Fair Cycle Detection
(Set Based Approach).
by I. Cerna, R. Pelanek
in Proceedings of Model Checking Software. 10th International SPIN Workshop
pages 49  73, volume 2648 of Lecture Notes of Computer Science, SpringerVerlag, 2003. Bibtex  Local Distributed Model Checking of
RegCTL.
by T. Brazdil, I. Cerna
In Proceedings of 1st International Workshop on Parallel and Distributed Model Checking PDMC'2002.
volume 68 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002. Bibtex  Property Driven Distribution of Nested DFS.
by J. Barnat, L. Brim and I. Cerna
in Proceedings of 3rd International Workshop on Verification and Computational Logic VCL'2002 Bibtex  Modifications of Expansion Trees for Weak
Bisimulation in BPA.
by J. Stribrna, I. Cerna
in Proceedings of 4th International Workshop on Verification of InfiniteState Systems Infinity'2002
Volume 68 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002. Bibtex  Distributed LTL ModelChecking Based on Negative
Cycle Detection.
by L. Brim, I. Cerna, P. Krcal and R. Pelanek
in Proceedings of 21st Conference Foundations of Software Technology and Theoretical Computer Science FSTTCS'01 pages 96  107, volume 2245 of Lecture Notes of Computer Science, SpringerVerlag, 2001. Bibtex  How to Employ Reverse Search in Distributed
SingleSource Shortest Paths.
by L. Brim, I. Cerna, P. Krcal and R. Pelanek
In Proceeding of 28th seminar on Current Trends in Theory and Practice of Informatics SOFSEM'01
pages 191  200, volume 2234 of Lecture Notes of Computer Science, SpringerVerlag, 2001. Bibtex  Randomization Helps in LTL Model Checking
by L. Brim, I. Cerna and M. Necesal
in Proceedings PAPMPROBMIV'01,
pages 105119, volume 2165 of Lecture Notes of Computer Science, SpringerVerlag , 2001. Bibtex  Pattern Equations and Equations with
Stuttering
by I. Cerna, O. Klima and J. Srba
Proceedings of 26th seminar on Current Trends in Theory and Practice of Informatics SOFSEM'99
pages 369378, volume 1725 of Lecture Notes of Computer Science, SpringerVerlag, 1999. Bibtex  Bisimilarity is Decidable in the Union of Normed BPA
and Normed BPP Processes.
by I. Cerna, M. Kretinsky, and A. Kucera.
In Proceedings of 1st International Workshop on Verification of Infinite State Systems INFINITY'96
volume 5 of Electronic Notes in Theoretical Computer Science, Elsevier Science, 1997 Bibtex  On the Relationship between Sequential and
Parallel Compositions in Process Algebras
by I. Cerna, M. Kretinsky, A. Kucera
In Proceedings of CSL96  The 1996 Annual Conference of the European Assoc.. Ultrech, The Netherlands: Department of Philosophy, Ulterech University, 1996. p. 1113. Bibtex  Some properties of zerotesting bounded oneway
multicounter machines.
by I. Cerna
In Proceedings of 15th International Symposium Mathematical Foundations of Computer Science MFCS'90
pages 195201, volume 452 of Lecture Notes of Computer Science, SpringerVerlag, 1990 Bibtex