Masaryk University

Publication Records

česky | in English

Filter publications

    2013

    1. Compositional Approach to Suspension and Other Improvements to LTL Translation
      BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Compositional Approach to Suspension and Other Improvements to LTL Translation. In Ezio Bartocci, C. R. Ramakrishnan. Model Checking Software - 20th International Symposium, SPIN 2013. LNCS 7976. Berlin Heidelberg: Springer, 2013, p. 81-98. ISBN 978-3-642-39175-0. Available from: https://dx.doi.org/10.1007/978-3-642-39176-7_6.
      RIV/00216224:14330/13:00066141 Proceedings paper. Informatics. English. United States of America.
      Babiak, Tomáš (703 Slovakia, belonging to the institution) -- Badie, Thomas (250 France) -- 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 time logic; model-checking; translation LTL to Buchi automata
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 15/11/2013 23:28.
      More: https://is.muni.cz/publication/1110031/en

    2012

    1. Model Checking for Communicating Quantum Processes.
      DAVIDSON, T, S J GAY, Hynek MLNAŘÍK, Rajagopal NAGARAJAN and N PAPANIKOLAOU. Model Checking for Communicating Quantum Processes. International Journal of Unconventional Computing. Old City Publishing, Inc., 2012, vol. 8, No 1, p. 73-98. ISSN 1548-7199.
      Abstract

      Keywords in English: Quantum computing; quantum communication; process calculus; model-checking; translation; semantics
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Hynek Mlnařík, Ph.D., učo 4326. Changed: 11/11/2012 10:57.
      More: https://is.muni.cz/publication/1072706/en

    2009

    1. DiVinE 2.0 (software)
      ROČKAI, Petr, Jiří BARNAT, Luboš BRIM and Milan ČEŠKA. DiVinE 2.0. 2009.
      URL
      Name in Czech: DiVinE 2.0
      Name (in English): DiVinE 2.0
      RIV/00216224:14330/09:00028810 Software. Informatics. English. Czech Republic.
      Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution) -- Češka, Milan (203 Czech Republic, belonging to the institution)
      Keywords in English: parallel verification; multi-core; model-checking; cluster; mpi
      International impact: yes
      Changed by: RNDr. Petr Ročkai, Ph.D., učo 139761. Changed: 18/2/2013 12:42.
      More: https://is.muni.cz/publication/875229/en
    2. On Decidability of LTL+Past Model Checking for Process Rewrite Systems
      KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). 2009th ed. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009, p. 105-117. ISSN 1571-0661.
      URL
      Name in Czech: O rozhodnutelnosti ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
      RIV/00216224:14330/09:00028439 Proceedings paper. Informatics. English. Portugal.
      Křetínský, Mojmír (203 Czech Republic) -- Řehák, Vojtěch (203 Czech Republic) -- Strejček, Jan (203 Czech Republic, guarantor)
      Keywords in English: process rewrite systems; LTL; infinite-state; model-checking; decidability
      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/6/2009 16:57.
      More: https://is.muni.cz/publication/800536/en

    2008

    1. DiVinE Cluster (software)
      BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Pavel ŠIMEČEK. DiVinE Cluster. 2008.
      URL
      Name in Czech: DiVinE Cluster
      Name (in English): DiVinE Cluster
      RIV/00216224:14330/08:00024473 Software. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic) -- Češka, Milan (203 Czech Republic) -- Šimeček, Pavel (203 Czech Republic)
      Keywords in English: cluster-based parallel verification; model-checking;
      International impact: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 23:17.
      More: https://is.muni.cz/publication/834419/en
    2. ProbDiVinE-MC (software)
      BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. ProbDiVinE-MC. 2008.
      URL
      Name in Czech: ProbDiVinE-MC
      Name (in English): ProbDiVinE-MC
      RIV/00216224:14330/08:00024418 Software. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic) -- Češka, Milan (203 Czech Republic) -- Tůmová, Jana (203 Czech Republic)
      Keywords in English: quantitative parallel verification; multi-core architecture; model-checking
      International impact: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 23:17.
      More: https://is.muni.cz/publication/813851/en

    2007

    1. Branching-Time Model-Checking of Probabilistic Pushdown Automata
      BRÁZDIL, Tomáš, Václav BROŽEK and Vojtěch FOREJT. Branching-Time Model-Checking of Probabilistic Pushdown Automata. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. Lisboa: Univerisity of Lisboa, 2007, p. 24-33.
      Name in Czech: Ověřování modelu pro logiky větvícího se času nad pravděpodobnostními zásobníkovými automaty
      Informatics. English. Portugal.
      Keywords in English: model-checking; Markov chains; temporal logics; probabilistic pushdown automata
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: Ing. Dana Komárková, učo 1475. Changed: 27/6/2008 09:30.
      More: https://is.muni.cz/publication/727767/en
    2. DiVinE Multi-Core (software)
      BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE Multi-Core. 2007.
      URL
      Name in Czech: DiVinE Multi-Core
      Name (in English): DiVinE Multi-Core
      RIV/00216224:14330/07:00019614 Software. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic, guarantor) -- Ročkai, Petr (203 Czech Republic)
      Keywords in English: parallel verification; multi-core architecture; model-checking
      International impact: yes
      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 12/2/2009 09:41.
      More: https://is.muni.cz/publication/759931/en
    3. On Decidability of LTL+Past Model Checking for Process Rewrite Systems
      KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. 2007.
      Name in Czech: Rozhodnutelnost ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
      RIV/00216224:14330/07:00019467 Presentations at conferences. Informatics. English. Portugal.
      Křetínský, Mojmír (203 Czech Republic, guarantor, belonging to the institution) -- Řehák, Vojtěch (203 Czech Republic, belonging to the institution) -- Strejček, Jan (203 Czech Republic, belonging to the institution)
      Keywords in English: process rewrite systems; LTL; infinite-state; model-checking; decidability
      Type of proceedings: pre-proceedings
      Type of participation: active participation (giving a lecture, organization, etc.)
      International impact: yes
      Reviewed: yes
      Changed by: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Changed: 28/4/2011 14:50.
      More: https://is.muni.cz/publication/723973/en
    4. ProbDiVinE (software)
      BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. ProbDiVinE. 2007.
      URL
      Name in Czech: ProbDiVinE
      Name (in English): ProbDiVinE
      RIV/00216224:14330/07:00024472 Software. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic) -- Češka, Milan (203 Czech Republic) -- Tůmová, Jana (203 Czech Republic)
      Keywords in English: qualitative parallel verification; model-checking; probabilistic systems
      International impact: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 22:47.
      More: https://is.muni.cz/publication/834418/en

    2005

    1. Assumption-based distribution of CTL model checking
      BRIM, Luboš, Jitka ŽIDKOVÁ and Karen YORAV. Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, vol. 7, No 1, p. 61-73, 14 pp. ISSN 1433-2779.
      Name in Czech: Distribuované ověřování modelu CTL založené na předpokladech
      Name (in English): Assumption-based distribution of CTL model checking
      RIV/00216224:14330/05:00012429 Article in a journal. Informatics. English. Germany.
      Brim, Luboš (203 Czech Republic, guarantor) -- Židková, Jitka (203 Czech Republic) -- Yorav, Karen (376 Israel)
      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.
      More: https://is.muni.cz/publication/569689/en
    2. DIVINE - The Distributed Verification Environment
      BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ and Pavel ŠIMEČEK. DIVINE - The Distributed Verification Environment. In In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisboa, Portugal: TU Munchen, 2005, p. 89-94.
      Name in Czech: DIVINE -- Prostředí pro distribuovanou verifikaci
      RIV/00216224:14330/05:00012768 Proceedings paper. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic, guarantor) -- Brim, Luboš (203 Czech Republic) -- Černá, Ivana (203 Czech Republic) -- Šimeček, Pavel (203 Czech Republic)
      Keywords in English: distributed; parallel; model-checking
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
      More: https://is.muni.cz/publication/589525/en
    3. DivSPIN - A SPIN compatible distributed model checker
      BARNAT, Jiří, Vojtěch FOREJT, Martin LEUCKER and Michael WEBER. DivSPIN - A SPIN compatible distributed model checker. In Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisabon, Portugalsko: TU Munchen, 2005, p. 95-100.
      Name in Czech: DivSPIN - distribuovaný model checker kompatibilní se SPINem
      RIV/00216224:14330/05:00013423 Proceedings paper. Informatics. English. Czech Republic.
      Barnat, Jiří (203 Czech Republic, guarantor) -- Forejt, Vojtěch (203 Czech Republic) -- Leucker, Martin (276 Germany) -- Weber, Michael (276 Germany)
      Keywords in English: distributed; parallel; model-checking; SPIN
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 10/1/2006 12:19.
      More: https://is.muni.cz/publication/589882/en
    4. Characteristic Patterns for LTL
      KUČERA, Antonín and Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg: Springer-Verlag, 2005, p. 239-249. ISBN 3-540-24302-X.
      Name in Czech: Charakteristické vzorce pro LTL
      RIV/00216224:14330/05:00012348 Proceedings paper. Informatics. English. Slovakia.
      Kučera, Antonín (203 Czech Republic, guarantor) -- Strejček, Jan (203 Czech Republic)
      Keywords in English: model-checking; linear temporal logic
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 29/3/2010 14:38.
      More: https://is.muni.cz/publication/563442/en
    5. Introductory paper: Parallel and Distributed Model Checking
      BRIM, Luboš and Orna GRUMBERG. Introductory paper: Parallel and Distributed Model Checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, vol. 7, No 1, p. 1-3. ISSN 1433-2779.
      Name in Czech: Úvodní článek: Paralelní a distribuované ověřování modelu
      Name (in English): Introductory paper: Parallel and Distributed Model Checking
      RIV/00216224:14330/05:00012428 Article in a journal. Informatics. English. Germany.
      Brim, Luboš (203 Czech Republic, guarantor) -- Grumberg, Orna (376 Israel)
      Keywords in English: model-checking
      International impact: yes
      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
      More: https://is.muni.cz/publication/569688/en

    2003

    1. Distribution of Explicit-State LTL Model-Checking
      BRIM, Luboš and Jiří BARNAT. Distribution of Explicit-State LTL Model-Checking. Editors Thomas Arts, Wan Fokking. Electronic Notes in Theoretical Computer Science. Elsevier Science, 2003, Volume 80, No 1, p. 120-125.
      URL
      Name (in English): Distribution of Explicit-State LTL Model-Checking
      RIV/00216224:14330/03:00008591 Article in a journal. Informatics. English. Netherlands.
      Brim, Luboš (203 Czech Republic, guarantor) -- Barnat, Jiří (203 Czech Republic)
      Keywords in English: model-checking; distribution; verification
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
      More: https://is.muni.cz/publication/489734/en
    2. Fast Mu-calculus Model Checking when Tree-width is Bounded
      OBDRŽÁLEK, Jan. Fast Mu-calculus Model Checking when Tree-width is Bounded. In CAV 2003. Berlin Heidelberg: Springer-Verlag, 2003, p. 80-92. ISBN 3-540-40524-0.
      RIV/00216224:14330/03:00008708 Proceedings paper. Informatics. English. Germany.
      Obdržálek, Jan (203 Czech Republic, guarantor)
      Keywords in English: parity games; mu-calculus; model-checking; tree-width
      Changed by: doc. Mgr. Jan Obdržálek, PhD., učo 1552. Changed: 26/5/2004 11:18.
      More: https://is.muni.cz/publication/555218/en
    3. Model checking LTL with regular valuations for pushdown systems
      ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON. Model checking LTL with regular valuations for pushdown systems. Information and Computation. Academic Press, 2003, vol. 186, No 2, p. 355-376. ISSN 0890-5401.
      RIV/00216224:14330/03:00008160 Article in a journal. Informatics. English. United States of America.
      Esparza, Javier (724 Spain) -- Kučera, Antonín (203 Czech Republic, guarantor) -- Schwoon, Stefan (276 Germany)
      Keywords in English: model-checking; liner-time logic; pushdown systems
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 18:17.
      More: https://is.muni.cz/publication/488376/en
    4. Parallel Algorithms for Detection of Negative Cycles
      BRIM, Lubos, Ivana ČERNÁ and Lukáš HEJTMÁNEK. Parallel Algorithms for Detection of Negative Cycles. In Proceedings of the 10th ParCo Conference. Holandsko: Elsevier B.V., 2003, p. 98-111.
      Name (in English): Parallel Algorithms for Detection of Negative Cycles
      RIV/00216224:14330/03:00008594 Proceedings paper. Informatics. English. Netherlands.
      Brim, Lubos (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic) -- Hejtmánek, Lukáš (203 Czech Republic)
      Keywords in English: model-checking; parallel computing
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
      More: https://is.muni.cz/publication/489815/en
    5. Parallel Algorithms for Detection of Negative Cycles
      BRIM, Lubos, Ivana ČERNÁ and Lukáš HEJTMÁNEK. Parallel Algorithms for Detection of Negative Cycles. Brno: Faculty of Informatics, 2003, 14 pp. Technical Reports, FIMU-RS-2003-04.
      URL
      Name (in English): Parallel Algorithms for Detection of Negative Cycles
      RIV/00216224:14330/03:00008564 Book on a specialized topic. Informatics. Czech. Czech Republic.
      Brim, Lubos (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic) -- Hejtmánek, Lukáš (203 Czech Republic)
      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.
      More: https://is.muni.cz/publication/488138/en

    2002

    1. INFINITY 2002. 4th International Workshop on Verification of Infinite-State Systems
      KUČERA, Antonín and Richard MAYR. INFINITY 2002. 4th International Workshop on Verification of Infinite-State Systems. 2002.
      URL
      Name (in English): INFINITY 2002. 4th International Workshop on Verification of Infinite-State Systems
      RIV/00216224:14330/02:00007778 Organization of a workshop. Information theory. English. Czech Republic.
      Kučera, Antonín (203 Czech Republic, guarantor) -- Mayr, Richard (276 Germany)
      Keywords in English: Infinite-State Systems; Formal Verification; Equivalence-Checking; Model-Checking
      International impact: yes
      Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 17:26.
      More: https://is.muni.cz/publication/486636/en
    2. Property Driven Distribution of Nested DFS
      BARNAT, Jiří, Luboš BRIM and Ivana ČERNÁ. Property Driven Distribution of Nested DFS. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic. Pittsburgh, PA, USA: Dept. of Electronics and Computer Science, University of Southampton, 2002, p. 1-10.
      Name (in English): Property Driven Distribution of Nested DFS
      RIV/00216224:14330/02:00006603 Proceedings paper. Informatics. English. United Kingdom of Great Britain and Northern Ireland.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic, guarantor) -- Černá, Ivana (203 Czech Republic)
      Keywords in English: model-checking; distributed model-checking; verification; verification tool
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 22/11/2006 16:02.
      More: https://is.muni.cz/publication/406260/en
    3. Using verified property to partition the state space in LTL model-checking
      BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes. Nantes, France: IRCCyN, Ecole Centrale de Nantes, 2002, p. 262-267.
      Name (in English): Using verified property to partition the state space in LTL model-checking
      RIV/00216224:14330/02:00006604 Proceedings paper. Informatics. English. France.
      Barnat, Jiří (203 Czech Republic, guarantor)
      Keywords in English: model-checking; distributed model-checking; verification
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 22/11/2006 16:01.
      More: https://is.muni.cz/publication/406263/en

    2001

    1. Distributed LTL Model-Checking in SPIN
      BARNAT, Jiří, Luboš BRIM and Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. In M.B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop. Toronto, Canada: Springer Verlag, 2001, p. 200-215. ISBN 3-540-42124-6.
      Name (in English): Distributed LTL Model-Checking in SPIN
      RIV/00216224:14330/01:00004189 Proceedings paper. Informatics. English. Canada.
      Barnat, Jiří (203 Czech Republic, guarantor) -- Brim, Luboš (203 Czech Republic) -- Stříbrná, Jitka (203 Czech Republic)
      Keywords in English: model-checking; verification; verification tool
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 22/11/2006 16:00.
      Identification numbers: 4200506714
      More: https://is.muni.cz/publication/362073/en

    2000

    1. Distributed LTL Model-Checking in SPIN
      BARNAT, Jiří, Luboš BRIM and Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. Brno: FI MU, 2000, 16 pp. Technical Reports.
      URL
      Name (in English): Distributed LTL Model-Checking in SPIN
      RIV/00216224:14330/00:00002823 Book on a specialized topic. Informatics. Czech. Czech Republic.
      Barnat, Jiří (203 Czech Republic) -- Brim, Luboš (203 Czech Republic) -- Stříbrná, Jitka (203 Czech Republic)
      Keywords in English: model-checking; verification; verification tool
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 26/5/2004 15:45.
      More: https://is.muni.cz/publication/346893/en
Displayed: 24/5/2024 05:49