Masaryk University

Publication Records

česky | in English

Filter publications

    2019

    1. 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.
      URL
      RIV/00216224:14330/19:00107786 Proceedings paper. English. Switzerland.
      Baier, Christel (276 Germany) -- Blahoudek, František (203 Czech Republic) -- Duret-Lutz, Alexandre (756 Switzerland) -- Klein, Joachim (276 Germany) -- Müller, David (276 Germany) -- Strejček, Jan (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: TELA; Emerson-Lei automata; emptiness check; probabilistic model checking
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 11:04.
    2. 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.
      URL
      RIV/00216224:14330/19:00107770 Proceedings paper. English. Switzerland.
      Major, Juraj (703 Slovakia, belonging to the institution) -- Blahoudek, František (203 Czech Republic) -- Strejček, Jan (203 Czech Republic, guarantor, belonging to the institution) -- Jánošová, Miriama (703 Slovakia, belonging to the institution) -- Zbončáková, Tatiana (703 Slovakia, belonging to the institution)
      Keywords in English: ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 00:04.

    2015

    1. 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.
      Name in Czech: O zpřesňování Büchiho automatů pro explicitní metodu ověřování modelu.
      RIV/00216224:14330/15:00080986 Proceedings paper. Informatics. English. Switzerland.
      Blahoudek, František (203 Czech Republic, belonging to the institution) -- Duret-Lutz, Alexandre (250 France) -- Rujbr, Vojtěch (203 Czech Republic, belonging to the institution) -- Strejček, Jan (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: linear temporal logic; Büchi automata; explicit model checking; specification refinement
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 20:47.

    2014

    1. 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.
      Name in Czech: Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
      RIV/00216224:14330/14:00073815 Proceedings paper. Informatics. English. United States of America.
      Blahoudek, František (203 Czech Republic, belonging to the institution) -- Duret-Lutz, Alexandre (250 France) -- Křetínský, Mojmír (203 Czech Republic, belonging to the institution) -- Strejček, Jan (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: linear temporal logic; Büchi automata; explicit model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 11/7/2019 13:31.

    2009

    1. 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.
      DOI
      Name in Czech: Skoro lineární Büchiho automaty
      RIV/00216224:14330/09:00029631 Proceedings paper. Informatics. English. Italy.
      Babiak, Tomáš (703 Slovakia) -- Řehák, Vojtěch (203 Czech Republic, guarantor) -- Strejček, Jan (203 Czech Republic)
      Keywords in English: LTL; linear time logic; model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 23/11/2009 16:12.
    2. CoIn Tool Set (software)
      URL
      Name in Czech: Sada nástrojů CoIn
      RIV/00216224:14330/09:00028846 Software. Informatics. English. Czech Republic.
      Beneš, Nikola (203 Czech Republic, guarantor, belonging to the institution) -- Bühnová, Barbora (203 Czech Republic, belonging to the institution) -- Černá, Ivana (203 Czech Republic, belonging to the institution) -- Křivánek, Milan (203 Czech Republic, belonging to the institution)
      Keywords in English: formal verification; model checking; component-interaction automata; state/event LTL
      International impact: yes

      Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 17/12/2010 12:26.
    3. 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.
      Name in Czech: Efektivní verifikace rosáhlých modelů
      Name (in English): Efficient Large-Scale Model Checking
      RIV/00216224:14330/09:00029324 Proceedings paper. Informatics. English. Italy.
      Verstoep, Kees (528 Netherlands) -- Bal, Henri E. (528 Netherlands) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution)
      Keywords in English: model checking; distributed; parallel; large-scale
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 2/2/2011 09:34.
    4. 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.
      URL
      Name in Czech: Algoritmická analýza transkripční regulace s využitím metody ověřování modelů
      RIV/00216224:14330/09:00029225 Article in a journal. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution) -- Černá, Ivana (203 Czech Republic, belonging to the institution) -- Dražan, Sven (203 Czech Republic, belonging to the institution) -- Fabriková, Jana (203 Czech Republic, belonging to the institution) -- Šafránek, David (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: Genetic regulatory network; Piecewise-linear approximation; Model checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 2/2/2011 09:33.
    5. 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.
      URL
      Name in Czech: O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy
      RIV/00216224:14330/09:00029078 Article in a journal. Informatics. English. Germany.
      Bozzelli, Laura (380 Italy) -- Křetínský, Mojmír (203 Czech Republic, guarantor) -- Řehák, Vojtěch (203 Czech Republic) -- Strejček, Jan (203 Czech Republic)
      Keywords in English: infinite-state systems; linear time logic; decidability; model checking
      International impact: yes
      Reviewed: yes

      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 22/5/2009 16:43.
    6. 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.
      URL
      Name in Czech: Prostorově efektivní ověřování modelu pro komponentově-interakční automaty
      RIV/00216224:14330/09:00028809 Proceedings paper. Informatics. English. Germany.
      Beneš, Nikola (203 Czech Republic, guarantor, belonging to the institution) -- Křivánek, Milan (203 Czech Republic, belonging to the institution) -- Štefaňák, Filip (703 Slovakia, belonging to the institution)
      Keywords in English: partial order reduction; model checking; component-based systems
      Type of proceedings: post-proceedings

      Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 17/12/2010 12:27.

    2008

    1. 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.
      Name in Czech: Komplementarita technik pro detekci chyb
      RIV/00216224:14330/08:00025027 Proceedings paper. Informatics. English. Netherlands.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Rosecký, Václav (203 Czech Republic) -- Moravec, Pavel (203 Czech Republic)
      Keywords in English: model checking; evaluation; error detection
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 30/3/2010 09:57.
    2. 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.
      Name in Czech: Boj se stavovou explozí: přehled a zhodnocení
      RIV/00216224:14330/08:00025026 Proceedings paper. Informatics. English. Germany.
      Pelánek, Radek (203 Czech Republic, guarantor)
      Keywords in English: model checking; state space explosion; review; evaluation; experience report
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 30/3/2010 09:52.
    3. 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.
      Name in Czech: Od jednoduchých regulačních motivů k ověřování komplexních transkripčních sítí
      RIV/00216224:14330/08:00024175 Proceedings paper. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic) -- Černá, Ivana (203 Czech Republic) -- Dražan, Sven (203 Czech Republic) -- Šafránek, David (203 Czech Republic, guarantor)
      Keywords in English: transcriptional networks; model checking; B. subtilis
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 31/3/2010 15:34.
    4. ŠIMEČEK, Pavel. I/O Efficient Model Checking. In Alpine Verification Meeting 2008. 2008.
      AVM 2008 web page
      Name in Czech: I/O-efektivní ověřování modelů
      Name (in English): I/O Efficient Model Checking
      Informatics. English. Austria.
      Keywords in English: external; I/O efficient; model checking; external memory
      Type of participation: active participation (giving a lecture, organization, etc.)
      International impact: yes

      Changed by: RNDr. Pavel Šimeček, Ph.D., učo 51636. Changed: 25/11/2008 14:06.
    5. 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.
      Name in Czech: Klasifikace modelů a automatická verifikace
      RIV/00216224:14330/08:00024587 Proceedings paper. Informatics. English. Germany.
      Pelánek, Radek (203 Czech Republic, guarantor)
      Keywords in English: model checking; automated verification; state space
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 23/6/2009 12:51.
    6. ŠAFRÁNEK, David. On Algorithmic Analysis of Biological Networks. In Control and System Theory Colloquium. 2008.
      Invited talk.
      Name in Czech: Algoritmická analýza biologických sítí
      RIV/00216224:14330/08:00028409 Requested lectures. Informatics. English. Czech Republic.
      Šafránek, David (203 Czech Republic, guarantor)
      Keywords in English: bilogical networks; model checking; systems biology
      Type of participation: active participation (giving a lecture, organization, etc.)
      International impact: yes

      Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 20/6/2008 14:24.
    7. 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.
      Name in Czech: Semi-externí ověřování LTL vlastností modelů
      Name (in English): Semi-external LTL Model Checking
      RIV/00216224:14330/08:00024282 Proceedings paper. Informatics. English. United States of America.
      Edelkamp, Stefan (276 Germany) -- Sanders, Peter (276 Germany) -- Šimeček, Pavel (203 Czech Republic, guarantor)
      Keywords in English: semi-external;model checking;external;I/O complexity
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Pavel Šimeček, Ph.D., učo 51636. Changed: 25/5/2009 11:42.
    8. Š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.
      Name in Czech: Semi-externí ověřování LTL vlastností modelů
      Name (in English): Semi-External LTL Model Checking
      Informatics. English. Czech Republic.
      Keywords in English: semi-external;model checking;external;I/O complexity
      Type of participation: active participation (giving a lecture, organization, etc.)
      International impact: yes

      Changed by: RNDr. Pavel Šimeček, Ph.D., učo 51636. Changed: 26/11/2008 09:05.
    9. 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.
      Name in Czech: CoIn Tool: Modelování a verifikace interakcí v komponentových systémech
      RIV/00216224:14330/08:00024294 Proceedings paper. Informatics. English. Spain.
      Beneš, Nikola (203 Czech Republic, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution) -- Černá, Ivana (203 Czech Republic, belonging to the institution) -- Sochor, Jiří (203 Czech Republic, belonging to the institution) -- Vařeková, Pavlína (203 Czech Republic, belonging to the institution) -- Zimmerová, Barbora (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: component-based systems; Component-Interaction automata; formal verification; LTL; model checking
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: RNDr. Nikola Beneš, Ph.D., učo 72525. Changed: 17/12/2010 12:32.

    2007

    1. 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.
      Name in Czech: Ověřování modelu pro rozsáhlé konečně stavové systémy a za jejich hranicemi
      RIV/00216224:14330/07:00019356 Proceedings paper. Informatics. English. Czech Republic.
      Brim, Luboš (203 Czech Republic, guarantor) -- Křetínský, Mojmír (203 Czech Republic)
      Keywords in English: finite and infinite-state systems; reachability; linear time logic; model checking; decidability
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Changed: 12/6/2008 09:40.
    2. 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.
      URL
      Name in Czech: Symbolicka verifikace slabe rozsirenych PAD
      RIV/00216224:14330/07:00021744 Proceedings paper. Informatics. English. Germany.
      Bouajjani, Ahmed (504 Morocco) -- Strejček, Jan (203 Czech Republic, guarantor) -- Touili, Tayssir (788 Tunisia)
      Keywords in English: rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 23/6/2009 17:48.
    3. 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.
      LMCS journal web-page.
      Name in Czech: Predikátová abstrakce a zjemňování dolních aproximací
      RIV/00216224:14330/07:00020179 Article in a journal. Informatics. English. Germany.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Pasareanu, Corina (642 Romania) -- Visser, Willem (710 South Africa)
      Keywords in English: model checking; predicate abstraction; under-approximation
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 23/6/2009 12:50.
    4. 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.
      Name in Czech: ProbDiVinE: Paralelní qualitativní model checker
      Name (in English): ProbDiVinE: A Parallel Qualitative LTL Model Checker
      RIV/00216224:14330/07:00019472 Proceedings paper. Informatics. English. United Kingdom of Great Britain and Northern Ireland.
      Barnat, Jiří (203 Czech Republic, guarantor) -- Brim, Luboš (203 Czech Republic) -- Černá, Ivana (203 Czech Republic) -- Češka, Milan (203 Czech Republic) -- Tůmová, Jana (203 Czech Republic)
      Keywords in English: ProbDiVinE; Qualitative LTL; Probabilistic; Model Checking
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 21:07.
    5. 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.
      Name in Czech: Oslabení podmínky na cykly zlepšující redukci pomocí reprezentantů
      Name (in English): Relaxed Cycle Condition Improves Partial Order Reduction
      RIV/00216224:14330/07:00019497 Proceedings paper. Informatics. English. Czech Republic.
      Moravec, Pavel (203 Czech Republic, guarantor) -- Šimša, Jiří (203 Czech Republic)
      Keywords in English: model checking; partial order reduction; proviso checking

      Changed by: Mgr. Pavel Moravec, učo 39589. Changed: 28/11/2007 10:10.
    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.
      Name in Czech: Logika pro náhodnostní hry
      RIV/00216224:14330/07:00022945 Proceedings paper. Informatics. English. United States of America.
      Baier, Christel (276 Germany) -- Brázdil, Tomáš (203 Czech Republic) -- Größer, Marcus (276 Germany) -- Kučera, Antonín (203 Czech Republic, guarantor)
      Keywords in English: stochastic systems; temporal logic; model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 25/11/2007 23:27.
    7. 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.
      Name in Czech: Verifikace VHDL programů s více hodinami pomocí SMV
      RIV/00216224:14330/07:00019329 Proceedings paper. Informatics. English. Germany.
      Smrčka, Aleš (203 Czech Republic) -- Řehák, Vojtěch (203 Czech Republic) -- Vojnar, Tomáš (203 Czech Republic) -- Šafránek, David (203 Czech Republic, guarantor) -- Matoušek, Petr (203 Czech Republic) -- Řehák, Zdeněk (203 Czech Republic)
      Keywords in English: formal verification; model checking; VHDL; asynchronous clock domains
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 9/4/2010 16:10.

    2006

    1. 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.
      Name in Czech: Experimentální porovnání algoritmů ověřujících proviso pro redukci pomocí reprezentantů
      Name (in English): Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction
      RIV/00216224:14330/06:00015445 Proceedings paper. Informatics. English. Czech Republic.
      Moravec, Pavel (203 Czech Republic, guarantor)
      Keywords in English: model checking; partial order reduction; proviso checking

      Changed by: Mgr. Pavel Moravec, učo 39589. Changed: 4/12/2006 15:24.
    2. 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.
      Name in Czech: Formální verifikace FIFO komponenty při návrhu síťového monitorovacího hardware
      RIV/00216224:14330/06:00015311 Proceedings paper. Informatics. English. Czech Republic.
      Kratochvíla, Tomáš (203 Czech Republic) -- Řehák, Vojtěch (203 Czech Republic) -- Šafránek, David (203 Czech Republic, guarantor)
      Keywords in English: formal verification; model checking; component-based hardware; FPGA
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. RNDr. David Šafránek, Ph.D., učo 3159. Changed: 9/4/2010 16:09.
    3. 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.
      Name in Czech: Využití horních a dolních mezí při zónových abstrakcích časových automatů
      RIV/00216224:14330/06:00015564 Article in a journal. Informatics. English. Germany.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Larsen, Kim G. (208 Denmark) -- Behrmann, Gerd (208 Denmark) -- Bouyer, Patricia (250 France)
      Keywords in English: model checking; timed automata; verification; abstraction; extrapolation
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:01.
    4. Č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.
      Name in Czech: Ověřování pro RegCTL
      RIV/00216224:14330/06:00015466 Article in a journal. Informatics. English. Slovakia.
      Černá, Ivana (203 Czech Republic, guarantor) -- Brázdil, Tomáš (203 Czech Republic)
      Keywords in English: model checking; RegCTL temporal logic
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 8/6/2009 16:06.
    5. Š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.
      Name in Czech: O alternativní konstrukci LTL tabla
      Name (in English): On Alternative Construction of LTL Tableau
      Informatics. English. Czech Republic.
      Keywords in English: model checking; linear temporal logic; tableau construction

      Changed by: Mgr. Jiří Šimša, učo 60360. Changed: 7/12/2006 12:13.
    6. 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.
      Name in Czech: O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy
      RIV/00216224:14330/06:00015417 Proceedings paper. Informatics. English. India.
      Bozzelli, Laura (380 Italy) -- Křetínský, Mojmír (203 Czech Republic, guarantor) -- Řehák, Vojtěch (203 Czech Republic) -- Strejček, Jan (203 Czech Republic)
      Keywords in English: infinite-state systems; linear time logic; decidability; model checking
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 20/12/2011 18:12.
    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.
      URL
      Name in Czech: O rozhodnutelnosti problému ověřování modelu pro LTL a slabě royšířené procesové přepisovací systémy
      RIV/00216224:14330/06:00015439 Audiovisual works. Informatics. English. Czech Republic.
      Bozzelli, Laura (380 Italy) -- Křetínský, Mojmír (203 Czech Republic, guarantor) -- Řehák, Vojtěch (203 Czech Republic) -- Strejček, Jan (203 Czech Republic)
      Keywords in English: infinite-state systems; linear time logic; decidability; model checking
      International impact: yes

      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 31/3/2010 15:19.
    8. 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.
      Name in Czech: Symbolicka verifikace slabe rozsirenych PAD
      RIV/00216224:14330/06:00018747 Proceedings paper. Informatics. English. Germany.
      Bouajjani, Ahmed (504 Morocco) -- Strejček, Jan (203 Czech Republic, guarantor) -- Touili, Tayssir (788 Tunisia)
      Keywords in English: rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 18/6/2007 14:11.

    2005

    1. 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.
      Name in Czech: Konkrétní hledání s abstraktním sdružováním a zjemněním
      RIV/00216224:14330/05:00012728 Proceedings paper. Informatics. English. United Kingdom of Great Britain and Northern Ireland.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Pasareanu, Corina (642 Romania) -- Visser, Willem (710 South Africa)
      Keywords in English: model checking; predicate abstraction; under-approximation
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:02.
    2. 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.
      Name in Czech: Hlubší spojitosti mezi LTL a alternujícími automaty
      RIV/00216224:14330/05:00012729 Proceedings paper. Informatics. English. France.
      Pelánek, Radek (203 Czech Republic) -- Strejček, Jan (203 Czech Republic, guarantor)
      Keywords in English: LTL; alternating automata; model checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 29/3/2010 12:50.
    3. BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005, 170 pp. PhD Thesis.
      Name in Czech: Ověřování modelu formulemi LTL v prostředís distribuovanou pamětí
      Name (in English): Distributed Memory LTL Model Checking (Ph.D. Thesis)
      RIV: Book on a specialized topic. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic, guarantor)
      Keywords in English: Distributed; LTL; Model Checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 23/6/2009 14:36.
    4. 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.
      URL
      Name in Czech: Jak se vypořádat s vyšší závislostí v partial order reduction při ověřování LTL vlastností modelu
      Name (in English): How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking
      RIV/00216224:14330/05:00012706 Proceedings paper. Informatics. English. Czech Republic.
      Moravec, Pavel (203 Czech Republic, guarantor)
      Keywords in English: model checking; partial order reduction; ample sets

      Changed by: Mgr. Pavel Moravec, učo 39589. Changed: 4/1/2007 12:22.
    5. 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.
      Name in Czech: O diskrétní sémantice časových automatů
      RIV/00216224:14330/05:00012726 Proceedings paper. Informatics. English. India.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Krčál, Pavel (203 Czech Republic)
      Keywords in English: model checking; timed automata; non-emptiness problems; decidability
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 23/6/2009 12:59.

    2004

    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.
      Name in Czech: Horní a dolní meze při analýze časových automatů s použitím zónové abstrakce
      RIV/00216224:14330/04:00010716 Proceedings paper. Informatics. English. Spain.
      Pelánek, Radek (203 Czech Republic, guarantor) -- Larsen, Kim G. (208 Denmark) -- Behrmann, Gerd (208 Denmark) -- Bouyer, Patricia (250 France)
      Keywords in English: model checking; timed automata; abstraction
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:02.
    2. 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.
      Name in Czech: Ověřování platnosti formulí temporálních logik pro procesy zásobníkových automatů
      RIV/00216224:14330/04:00010191 Proceedings paper. Informatics. English. United States of America.
      Esparza, Javier (724 Spain) -- Kučera, Antonín (203 Czech Republic, guarantor) -- Mayr, Richard (276 Germany)
      Keywords in English: Probabilistic Pushdown Automata; Model Checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 17:28.
    3. BRIM, Luboš. Parallel Model-Checking. ERCIM News. ERCIM EEIG, 2004, vol. 58, June, p. 35-36. ISSN 0926-4981.
      URL
      Name in Czech: Paralelní ověřování modelu
      Name (in English): Parallel Model-Checking
      RIV/00216224:14330/04:00010182 Article in a journal. Informatics. Czech. Czech Republic.
      Brim, Luboš (203 Czech Republic, guarantor)
      Keywords in English: Model Checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.

    2003

    1. 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.
      Name (in English): LTL Hierarchies and Model Checking
      RIV/00216224:14330/03:00008596 Proceedings paper. Informatics. English. Austria.
      Pelánek, Radek (203 Czech Republic, guarantor)
      Keywords in English: LTL; model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes

      Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 21/11/2006 14:02.
    2. 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.
      RIV/00216224:14330/03:00008593 Proceedings paper. Informatics. English. Canada.
      Barnat, Jiří (203 Czech Republic, guarantor) -- Brim, Luboš (203 Czech Republic) -- Chaloupka, Jakub (203 Czech Republic)
      Keywords in English: model checking; parallel algorithm; breadth first search
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 21:17.
    3. BRIM, Luboš and Orna GRUMBERG. PDMC 2003 - Parallel and Distributed Model Checking. Proceedings. Nizozemsko: Elsevier, 2003, 130 pp. ENTCS, Vol. 89, No. 1.
      Name (in English): PDMC 2003 - Parallel and Distributed Model Checking. Proceedings.
      RIV/00216224:14330/03:00008595 Book on a specialized topic. Informatics. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Grumberg, Orna (376 Israel)
      Keywords in English: model checking; parallel computing; distributed computing
      International impact: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
    4. Č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.
      RIV/00216224:14330/03:00008590 Proceedings paper. Informatics. English. Germany.
      Černá, Ivana (203 Czech Republic, guarantor) -- Pelánek, Radek (203 Czech Republic)
      Keywords in English: temporal logic; automata over infinite words; model checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 8/6/2009 16:09.
      Identification numbers: 4200509002
    5. 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.
      URL
      RIV/00216224:14330/03:00008592 Proceedings paper. Informatics. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Žídková, Jitka (203 Czech Republic)
      Keywords in English: verification; model checking

      Changed by: Mgr. Jitka Žídková, učo 2922. Changed: 26/5/2004 16:19.
    6. ŽÍ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.
      Name (in English): Using Assumptions to Distribute Model Checking
      RIV/00216224:14330/03:00008254 Proceedings paper. Informatics. English. Czech Republic.
      Žídková, Jitka (203 Czech Republic, guarantor)
      Keywords in English: verification; model checking; distribution

      Changed by: Mgr. Jitka Žídková, učo 2922. Changed: 26/5/2004 16:20.
    7. 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.
      URL
      RIV/00216224:14330/03:00008325 Audiovisual works. Informatics. English. Czech Republic.
      Kratochvíla, Tomáš (203 Czech Republic) -- Řehák, Vojtěch (203 Czech Republic, guarantor) -- Šimeček, Pavel (203 Czech Republic)
      Keywords in English: Liberouter; Combo6; formal verification; hardware verification; model checking; Cadence SMV; LeonardoSpectrum

      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 18/10/2004 15:55.

    2002

    1. Č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.
      Name (in English): Local Distributed Model Checking of RegCTL
      RIV/00216224:14330/02:00006437 Proceedings paper. Informatics. English. Netherlands.
      Černá, Ivana (203 Czech Republic, guarantor) -- Brázdil, Tomáš (203 Czech Republic)
      Keywords in English: model checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 22/11/2006 15:07.
    2. 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.
      URL
      Computer hardware and software. English. Czech Republic.
      Keywords in English: model checking; hardware design

      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 20/12/2004 12:13.
    3. BRIM, Luboš and Orna GRUMBERG. PDMC 2002 - Parallel and Distributed Model Checking. 2002.
      Name (in English): PDMC 2002 - Parallel and Distributed Model Checking.
      RIV/00216224:14330/02:00007762 Organization of a workshop. Computer hardware and software. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Grumberg, Orna (376 Israel)
      Keywords in English: model checking; parallel computing
      International impact: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
    4. 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.
      Name (in English): PDMC 2002 - Parallel and Distributed Model Checking. Proceedings.
      RIV/00216224:14330/02:00006419 Book on a specialized topic. Computer hardware and software. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Grumberg, Orna (376 Israel)
      Keywords in English: model checking; parallel computing
      International impact: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
    5. 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.
      Name (in English): Using Assumptions to Distribute CTL Model Checking
      RIV/00216224:14330/02:00006432 Proceedings paper. Computer hardware and software. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Crhová, Jitka (203 Czech Republic) -- Yorav, Karen (376 Israel)
      Keywords in English: verification; model checking
      International impact: yes
      Reviewed: yes

      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.

    2001

    1. 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.
      RIV/00216224:14330/01:00004526 Proceedings paper. Information theory. English. Germany.
      Keywords in English: Model checking; randomized algorithm; depth-first search

      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 31/10/2001 08:01.
Displayed: 19/9/2024 13:47