Ivana Cerna

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.

DPLB , Google Scholar

• On clock-aware LTL parameter synthesis of timed automata
  by P. Bezdek, N. Benes, I. Cerna and J. Barnat
  J. Log. Algebr. Meth. Program vol. 99, pp. 114-142, 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. 230-253, 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. 1-14, 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. 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), pp. 261-266, 2013 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

• 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. 189--204, 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. 1099-1104, 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:1--50:13, Schloss Dagstuhl--Leibniz-Zentrum 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. 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