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
- 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. 1-14, 2015. Bibtex -
Formal analysis of piecewise affine systems through formula-guided refinement.
by B. Yordanov, J. Tumova, I. Cerna, J. Barnat, C. Belta
In Automatica, volume 49(1), 2013, 261-266. Bibtex - Temporal
Logic Control of Discrete-Time 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. 1491-1504, 2012. Bibtex - Verification of Systems with Degradation
by J. Barnat, I. Cerna, J. Tumova
In Computing and Informatics, vol. 31, pp. 507-530, 2012. Bibtex -
Partial Order Reduction for State/Event LTL with Application to
Component-Interaction 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. 877-890, 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 0304-3975, 2009, vol. 2009, no. 410, s. 3128-3148. 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, 532--546. Bibtex - Model
checking of RegCTL.
by T. Brazdil and I. Cerna
In Computing and Informatics, 2006, vol. 25, n. 1, p. 81-97. Bibtex - Comparing Expressibility of Normed BPA and
Normed BPP Processes.
by I. Cerna, M. Kretinsky, and A. Kucera.
Acta Informatica, 36(3):233-256. Springer, 1999 Bibtex -
Distributed Breadth-First 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, 117-134(18). Bibtex
- Separation of deterministic, nondeterministic and
alternating complexity classes.
by A. Bebjak, I. Stefanekova
Theoretical Computer Science, 88:297-311, 1991 Bibtex - Nondeterministic multicounter machines and
complementation.
by D. Pardubska, I. Stefanekova
Theoretical Computer Science,67:111-113, 1989. Bibtex - Relation between one-time-only branching programs and
real-time branching programs.
by A. Bebjak, I. Stefanekova
Computers and Artificial Intelligence, 7:107-111, 1988 Bibtex - Nondeterminism is essential for
reversal-bounded
two-way multihead automata.
by A. Bebjak, I. Stefanekova
Kybernetika,24:65-71, 1988. Bibtex
Proceedings
- 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. 172-187. 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. 121-136. 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. 1238-1243. 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. 259-268. 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. 259-268. 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. 28-39. Bibtex - On
Clock-Aware 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, 46-60. Bibtex - Towards
Verification of Ensemble-Based 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, 1-20. 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 Component-based software engineering, ACM, 2013, CBSE '13, 43--52. 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. 3938-3943, 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. 4399-4404, 2013. Bibtex -
Attraction-based 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. 6749-6754, 2012. Bibtex -
Factorization for Component-Interaction Automata
by N. Benes, I. Cerna, F. Stefanak
In Proceedings of SOFSEM 2012: Theory and Practice of Computer Science. LNCS 7147, pp. 554-565, 2012. Bibtex - Reliability Analysis
in Component-based 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. 83-92, 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. 14869-14875, 2011. Bibtex - CoInDiVinE: Parallel Distributed Model
Checker for Component-Based 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. 63-67. 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. 228-242, 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. 4230-4235, 2010. Bibtex - Formal
Analysis of Piecewise Affine Systems through Formula-Guided Refinement
by B. Yordanov, J. Tumova, C. Belta, I. Cerna, J. Barnat
In Proceedings of IEEE Conference on Decision and Control (CDC), pp. 5899-5904, 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, 31-45. Bibtex - BioDiVinE: A Tool for Parallel Analysis of
Multi-Affine 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 TR-09-09 of Technical Report, 1--5. Bibtex - Computational Analysis of Large-Scale
Multi-Affine 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, 81-90. 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), Springer-Verlag, 2009, volume 5423 of LNCS, 307--321. 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, 21-30. 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. 53-68, 2008. Bibtex -
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems
by P. Varekova, I. Varekova, I. Cerna
In Proceedings of Proceedings of FACS'08, 2008, 41--55. Bibtex - Model
Checking of Control-User Component-Based Parametrised Systems
by P. Varekova, I. Cerna
In Proceedings of CBSE'08, Springer, 2008, volume 5282 of Lecture Notes in Computer Science, 146-162. Bibtex -
Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE
by J. Barnat, L. Brim, I. Cerna, S. Drazan, D. Safranek
In ENTCS, volume 194(3), 2008, 35--50. Bibtex - ProbDiVinE-MC: Multi-core 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, 77--78. Bibtex - A Case Study in Parallel Verification of
Component-Based Systems
by N. Benes, J. Cerna, J. Sochor, P. Varekova, B. Zimmerova
In Electr. Notes Theor. Comput. Sci., volume 220(2), 2008, 67-83. Bibtex - The CoIn Tool: Modelling and Verification of
Interactions in Component-Based 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, 221--225. Bibtex - Component-Interaction 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. 83-96, 2008. Bibtex -
Component Substitutability via Equivalencies of Component-Interaction Automata
by I. Cerna, P. Varekova, B. Zimmerova
In Electronic Notes in Theoretical Computer Science, volume 182, June 2007, 39--55. 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 Component-Based Systems (SAVCBS'07), ACM Press, 2007, 3--13. 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, 215-216. Bibtex - Cluster-Based 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. 259-279. Bibtex - Component Substitutability via Equivalencies of Component-Interaction Automata
by I. Cerna, O. Varekova, B. Zimmerova
In Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06). Macao: UNU-IIST, 2006. p. 115-130. Bibtex - How to Order Vertices for Distributed
LTL Model-Checking 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 3-18, 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 -
Component-Interaction Automata as a Verification-Oriented
Component-Based System Specification.
by B. Zimmerova, L. Brim, I. Cerna and P. Varekova
in Specification and Verification of Component-Based Systems (SAVCBS 05),
pages 352 - 366, , 2005. Bibtex - Accepting Predecessors are Better than Back
Edges in Distributed LTL Model-Checking.
by L. Brim, I. Cerna, P. Moravec and J. Simsa
in Proc. Formal Methods in Computer-Aided Design (FMCAD2004),
pages 352 - 366, volume 3312 of Lecture Notes of Computer Science, Springer-Verlag, 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, Springer-Verlag, 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, Springer-Verlag, 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 Infinite-State Systems Infinity'2002
Volume 68 of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, 2002. Bibtex - Distributed LTL Model-Checking 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 FST-TCS'01 pages 96 - 107, volume 2245 of Lecture Notes of Computer Science, Springer-Verlag, 2001. Bibtex - How to Employ Reverse Search in Distributed
Single-Source 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, Springer-Verlag, 2001. Bibtex - Randomization Helps in LTL Model Checking
by L. Brim, I. Cerna and M. Necesal
in Proceedings PAPM-PROBMIV'01,
pages 105-119, volume 2165 of Lecture Notes of Computer Science, Springer-Verlag , 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 369-378, volume 1725 of Lecture Notes of Computer Science, Springer-Verlag, 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. 11-13. Bibtex - Some properties of zerotesting bounded one-way
multicounter machines.
by I. Cerna
In Proceedings of 15th International Symposium Mathematical Foundations of Computer Science MFCS'90
pages 195-201, volume 452 of Lecture Notes of Computer Science, Springer-Verlag, 1990 Bibtex