Publication Records

BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER and Jan STREJČEK. Generic Emptiness Check for Fun and Profit. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, p. 445-461. ISBN 978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3_26.

MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ and Tatiana ZBONČÁKOVÁ. ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, p. 357-365. ISBN 978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3_21.

BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR and Jan STREJČEK. On Refinement of Büchi Automata for Explicit Model Checking. In Fischer, Bernd and Geldenhuys, Jaco. 2015 International SPIN Symposium on Model Checking of Software. Heidelberg, New York, Dordrecht, London: Springer International Publishing, 2015, p. 66-83. ISBN 978-3-319-23403-8. Available from: https://dx.doi.org/10.1007/978-3-319-23404-5_6.

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Is there a best Büchi automaton for explicit model checking? In Neha Rungta and Oksana Tkachuk. 2014 International SPIN Symposium on Model Checking of Software. New York: ACM, 2014, p. 68-76. ISBN 978-1-4503-2452-6. Available from: https://dx.doi.org/10.1145/2632362.2632377.

BABIAK, Tomáš, Vojtěch ŘEHÁK and Jan STREJČEK. Almost Linear Büchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). 1st ed. internet: EPTCS, 2009, p. 16-25. ISSN 2075-2180.

BENEŠ, Nikola, Barbora BÜHNOVÁ, Ivana ČERNÁ and Milan KŘIVÁNEK. CoIn Tool Set. 2009.

VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT and Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009, p. 201-212. ISBN 978-1-4244-3751-1.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ and David ŠAFRÁNEK. On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science. 2009, vol. 2009, No 410, p. 3128-3148, 20 pp. ISSN 0304-3975.

BOZZELLI, Laura, 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. Berlin: Springer-Verlag, 2009, vol. 46, No 1, p. 1-28. ISSN 0001-5903.

BENEŠ, Nikola, Milan KŘIVÁNEK and Filip ŠTEFAŇÁK. Space Effective Model Checking for Component-Interaction Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Dagstuhl, Německo: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo, 2009, 8 pp. ISBN 978-3-939897-15-6.

PELÁNEK, Radek, Václav ROSECKÝ and Pavel MORAVEC. Complementarity of Error Detection Techniques. In Parallel and Distributed Methods in verifiCation (PDMC 2008). Nizozemsko: Elsevier, 2008, 14 pp. ISSN 1571-0661.

PELÁNEK, Radek. Fighting State Space Explosion: Review and Evaluation. In Formal Methods for Industrial Critical Systems. Německo: Springer, 2008, 15 pp. ISBN 3-642-03239-7.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN and David ŠAFRÁNEK. From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks. In Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation. Budapest: Ivana Cerna and Gerald Luettgen, 2008, p. 83-96, 15 pp. ISSN 1571-0661.

ŠIMEČEK, Pavel. I/O Efficient Model Checking. In Alpine Verification Meeting 2008. 2008.

PELÁNEK, Radek. Model Classifications and Automated Verification. In Formal Methods for Industrial Critical Systems. Německo: Springer, 2008, p. 149-163. ISBN 978-3-540-79706-7.

ŠAFRÁNEK, David. On Algorithmic Analysis of Biological Networks. In Control and System Theory Colloquium. 2008.

EDELKAMP, Stefan, Peter SANDERS and Pavel ŠIMEČEK. Semi-external LTL Model Checking. In 20th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2008, p. 530-542. ISBN 978-3-540-70543-7.

ŠIMEČEK, Pavel. Semi-External LTL Model Checking. Co-authors of the original paper in CAV 2008 proceedings. In EDELKAMP, Stefan and Peter SANDERS. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2008. ISBN 978-80-7355-082-0.

BENEŠ, Nikola, 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. In Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08). Málaga, Spain: Department of Computer Science, University of Málaga, 2008, p. 221-225. ISSN 1571-0661.

BRIM, Luboš and Mojmír KŘETÍNSKÝ. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2007, p. 9-28. ISBN 978-3-540-69506-6.

BOUAJJANI, Ahmed, Jan STREJČEK and Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006). Neuveden: Elsevier, 2007, p. 47-64. ISSN 1571-0661.

PELÁNEK, Radek, Corina PASAREANU and Willem VISSER. Predicate Abstraction with Under-Approximation Refinement. Logical Methods in Computer Science. Germany: Technical University of Braunschweig, 2007, vol. 3, No 1, p. 1-22. ISSN 1860-5974.

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. ProbDiVinE: A Parallel Qualitative LTL Model Checker. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07). United States of America: IEEE Computer Society, 2007, p. 215-216. ISBN 0-7695-2883-X.

MORAVEC, Pavel and Jiří ŠIMŠA. Relaxed Cycle Condition Improves Partial Order Reduction. In 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo, Czech Republic: FI MU, FIT VUT, 2007, p. 140-147. ISBN 978-80-7355-077-6.

BAIER, Christel, Tomáš BRÁZDIL, Marcus GRÖSSER and Antonín KUČERA. Stochastic Game Logic. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007). Los Alamitos, Washington, Tokyo: IEEE Computer Society, 2007, p. 227-236. ISBN 0-7695-2883-X.

SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK and Zdeněk ŘEHÁK. Verifying VHDL Designs with Multiple Clocks in SMV. In Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006. Bonn: Springer-Verlag, 2007, p. 148-164, 16 pp. ISBN 978-3-540-70951-0.

MORAVEC, Pavel. Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic: FI MU Report Series, 2006, p. 129-136.

KRATOCHVÍLA, Tomáš, Vojtěch ŘEHÁK and David ŠAFRÁNEK. Formal Verification of a FIFO Component in Design of Network Monitoring Hardware. In 10 years of CESNET - CESNET CONFERENCE 2006. Praha: CESNET, z.s.p.o., 2006, p. 151-160. ISBN 978-80-239-6533-9.

PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2006, vol. 8, No 3, p. 204-215. ISSN 1433-2779.

ČERNÁ, Ivana and Tomáš BRÁZDIL. Model Checking of RegCTL. Computing and Informatics. 2006, vol. 25, No 1, p. 81-97, 16 pp. ISSN 1335-9150.

ŠIMŠA, Jiří. On Alternative Construction of LTL Tableau. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic: FI MU Report Series, 2006, p. 222-229.

BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK and Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006, p. 248-259. ISBN 978-3-540-49994-7.

BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK and Jan STREJČEK. On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Brno: FI MU, 2006. FIMU-RS-2006-05.

BOUAJJANI, Ahmed, Jan STREJČEK and Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06. London: Imperial College London, 2006, p. 29-41.

PELÁNEK, Radek, Corina PASAREANU and Willem VISSER. Concrete Search with Abstract Matching and Refinement. In Computer Aided Verification. Edinburgh: Springer, 2005, p. 52-66. ISBN 3-540-27231-3.

PELÁNEK, Radek and Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005, p. 238-249. ISBN 978-3-540-31023-5.

BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005, 170 pp. PhD Thesis.

MORAVEC, Pavel. How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking. In 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005). Znojmo, Czech Republic: FI MU Report Series, 2005, p. 186-192.

PELÁNEK, Radek and Pavel KRČÁL. On Sampled Semantics of Timed Systems. In Foundations of Software Technology and Theoretical Computer Science. India: Springer, 2005, p. 310-321. ISBN 978-3-540-30495-1.

PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN and Patricia BOUYER. Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. In Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004). Barcelona (Španělsko): Springer-Verlag, 2004, p. 312-326. ISBN 3-540-21299-X.

ESPARZA, Javier, Antonín KUČERA and Richard MAYR. Model Checking Probabilistic Pushdown Automata. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004). Los Alamitos (California): IEEE Computer Society, 2004, p. 12-21. ISBN 0-7695-2192-4.

BRIM, Luboš. Parallel Model-Checking. ERCIM News. ERCIM EEIG, 2004, vol. 58, June, p. 35-36. ISSN 0926-4981.

PELÁNEK, Radek. LTL Hierarchies and Model Checking. In Proceedings of the Eight ESSLLI Student Session. Wien: TU Wien, 2003, p. 245-254, 9 pp.

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03). Montreal: IEEE Computer Society, 2003, p. 106-115. ISBN 0-7695-2035-9.

BRIM, Luboš and Orna GRUMBERG. PDMC 2003 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2003, 130 pp. ENTCS, Vol. 89, No. 1.

ČERNÁ, Ivana and Radek PELÁNEK. Relating Hierarchy of Temporal Properties to Model Checking. In Mathematical Foundations of Computer Science (MFCS 2003). Bratislava (Slovensko): Springer-Verlag, 2003, p. 318-327. ISBN 3-540-40671-9.

BRIM, Luboš and Jitka ŽÍDKOVÁ. Using Assumptions to Distribute Alternation Free mu-Calculus Model Checking. In 2st International Workshop on Parallel and Distributed Model Checking (PDMC 2003). Boulder, Colorado, USA. Brno, Czech Republic: Elsevier, 2003, p. 19-34.

ŽÍDKOVÁ, Jitka. Using Assumptions to Distribute Model Checking. In Počítačové Architektury & Diagnostika. Brno, Česká republika: Vysoké učení technické v Brně, Fakulta Informačních technologií, Ustav počítačových systémů, 2003, p. 73-78. ISBN 80-214-2471-0.

KRATOCHVÍLA, Tomáš, Vojtěch ŘEHÁK and Pavel ŠIMEČEK. Verification of COMBO6 VHDL Design. Praha: CESNET, z.s.p.o., 2003. CESNET Technical Report No. 17/2003.

ČERNÁ, Ivana and Tomáš BRÁZDIL. Local Distributed Model Checking of RegCTL. In PDMC 2002 Parallel and Distributed Model Checking. The Netherlands: Elsevier Science Publishers, 2002, p. 1-14. ISBN 0444512918.

BARNAT, Jiří, Tomáš BRÁZDIL, Pavel KRČÁL, Vojtěch ŘEHÁK and David ŠAFRÁNEK. Model checking in IPv6 Hardware Router Design. Praha: CESNET, z. s. p. o., 2002. CESNET technical report number 8/2002.

BRIM, Luboš and Orna GRUMBERG. PDMC 2002 - Parallel and Distributed Model Checking. 2002.

BRIM, Luboš and Orna GRUMBERG. PDMC 2002 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2002, 165 pp. ENTCS, Vol. 68, No. 4. ISBN 0444512918.

BRIM, Luboš, Jitka CRHOVÁ and Karen YORAV. Using Assumptions to Distribute CTL Model Checking. In 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002). Brno, Czech Republic: Elsevier, 2002, p. 80-95. ISBN 0444512918.

BRIM, Luboš, Ivana ČERNÁ and Martin NEČESAL. Randomization Helps in LTL Model Checking. In Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001. Berlin Heidelberg New York: Springer, 2001, p. 105-119. LNCS 2165. ISBN 3-540-42556-X.