Masarykova univerzita

Výpis publikací

česky | in English

Filtrování publikací

    2024

    1. JONÁŠ, Martin, Jan STREJČEK, Marek TRTÍK a Lukáš URBAN. Fizzer: New Gray-Box Fuzzer. Online. In Dirk Beyer and Ana Cavalcanti. Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings. Cham (Švýcarsko): Springer, 2024, s. 309-313. ISBN 978-3-031-57258-6. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57259-3_17.
      URL
      RIV: Stať ve sborníku. angličtina. Německo.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika, domácí) -- Urban, Lukáš (703 Slovensko, domácí)
      Klíčová slova anglicky: fuzzing; test generation; atomic Boolean expression; Fizzer
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 24. 4. 2024 13:49.
    2. JONÁŠ, Martin, Jan STREJČEK, Marek TRTÍK a Lukáš URBAN. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 90-109. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_5.
      URL
      RIV: Stať ve sborníku. angličtina. Německo.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika, domácí) -- Urban, Lukáš (703 Slovensko, domácí)
      Klíčová slova anglicky: fuzzing; test generation; atomic Boolean expression; Fizzer
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 24. 4. 2024 13:33.
    3. AYAZIOVÁ, Paulína, Dirk BEYER, Marian LINGSCH-ROSENFELD, Martin SPIESSL a Jan STREJČEK. Software Verification Witnesses 2.0. Online. In Thomas Neele and Anton Wijs. Model Checking Software - 30th International Symposium, SPIN 2024. Cham (Švýcarsko): Springer, 2024, s. 184-204.
      angličtina. Německo.
      Klíčová slova anglicky: verification witnesses; software verification; validation; exchange format; invariant; counterexample
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 26. 8. 2024 14:52.
    4. JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ a Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 406-411. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_29.
      URL
      RIV: Stať ve sborníku. angličtina. Německo.
      Jonáš, Martin (203 Česká republika, garant, domácí) -- Kumor, Kristián (703 Slovensko, domácí) -- Novák, Jakub (703 Slovensko, domácí) -- Sedláček, Jindřich (203 Česká republika, domácí) -- Trtík, Marek (203 Česká republika, domácí) -- Zaoral, Lukáš (203 Česká republika) -- Ayaziová, Paulína (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution; software verification; Symbiotic
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 24. 4. 2024 13:32.
    5. JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Cham: Springer, 2024, s. 234-255. ISBN 978-3-031-57227-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57228-9_12.
      URL
      RIV: Stať ve sborníku. angličtina. Německo.
      Jankola, Marek (703 Slovensko) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: tight automata; shortest counterexamples; LTL
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 4. 2024 18:31.
    6. AYAZIOVÁ, Paulína a Jan STREJČEK. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 341-346. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_18.
      URL
      RIV: Stať ve sborníku. angličtina. Německo.
      Ayaziová, Paulína (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Witch;witness-validator;SV-COMP;verification witness
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 4. 2024 18:51.

    2023

    1. SCHWARZOVÁ, Tereza, Jan STREJČEK a Juraj MAJOR. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. Online. In Meena Mahajan and Friedrich Slivovsky. 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, s. 1-20. ISBN 978-3-95977-286-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2023.23.
      URL
      RIV/00216224:14330/23:00131935 Stať ve sborníku. angličtina. Německo.
      Schwarzová, Tereza (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Major, Juraj (703 Slovensko, domácí)
      Klíčová slova anglicky: Emerson-Lei automata; TELA; automata reduction; QBF; telatko
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 19. 3. 2024 13:57.
    2. AYAZIOVÁ, Paulína a Jan STREJČEK. Symbiotic-Witch 2. 2023.
      Odkaz na stránku software
      angličtina. Česká republika.
      Klíčová slova anglicky: Witch;witness-validator;SV-COMP;verification witness
      Mezinárodní význam: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 7. 11. 2023 15:49.
    3. AYAZIOVÁ, Paulína a Jan STREJČEK. Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation. Online. In Sriram Sankaranarayanan and Natasha Sharygina. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2023, s. 523-528. ISBN 978-3-031-30819-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-30820-8_30.
      URL
      RIV/00216224:14330/23:00131936 Stať ve sborníku. angličtina. Švýcarsko.
      Ayaziová, Paulína (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Witch;witness-validator;SV-COMP;verification witness
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 7. 4. 2024 23:35.

    2022

    1. BEYER, Dirk a Jan STREJČEK. Case Study on Verification-Witness Validators: Where We Are and Where We Go. Online. In Gagandeep Singh, Caterina Urban. Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings. Cham (Switzerland): Springer, 2022, s. 160-174. ISBN 978-3-031-22307-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-22308-2_8.
      URL
      RIV/00216224:14330/22:00127777 Stať ve sborníku. angličtina. Švýcarsko.
      Beyer, Dirk (276 Německo) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: software verification;program analysis;software validation;software bugs;verification witnesses;evaluation;benchmarking
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 3. 2023 12:08.
    2. CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. Online. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2022, s. 462-467. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_32.
      URL
      RIV/00216224:14330/22:00125696 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, domácí) -- Mihalkovič, Vincent (703 Slovensko, domácí) -- Řechtáčková, Anna (203 Česká republika, domácí) -- Zaoral, Lukáš (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic;BSELF;SV-COMP;program analysis;verification
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 3. 2023 12:49.
    3. Symbiotic 9.1 (software)
      CHALUPA, Marek, Jakub NOVÁK, Marek TRTÍK, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9.1. 2022.
      Odkaz na stránku software
      angličtina. Česká republika.
      Klíčová slova anglicky: Symbiotic; symbolic execution; slicing; bug-finding
      Mezinárodní význam: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 7. 11. 2023 15:16.
    4. AYAZIOVÁ, Paulína, Marek CHALUPA a Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2022, s. 468-473. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_33.
      URL
      RIV/00216224:14330/22:00125695 Stať ve sborníku. angličtina. Švýcarsko.
      Ayaziová, Paulína (703 Slovensko, domácí) -- Chalupa, Marek (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic;witness-validator;SV-COMP;verification witness
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 3. 2023 10:40.

    2021

    1. CHALUPA, Marek a Jan STREJČEK. Backward Symbolic Execution with Loop Folding. Online. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi. Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 49-76. ISBN 978-3-030-88805-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-88806-0_3.
      URL
      RIV/00216224:14330/21:00122663 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution;k-induction;backward symbolic execution;inductive invariants;invariants
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 5. 2022 15:01.
    2. SÍČ, Juraj a Jan STREJČEK. DQBDD: An Efficient BDD-Based DQBF Solver. Online. In Chu-Min Li and Felip Manyà. Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 535-544. ISBN 978-3-030-80222-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-80223-3_36.
      URL
      RIV/00216224:14330/21:00122203 Stať ve sborníku. angličtina. Švýcarsko.
      Síč, Juraj (703 Slovensko) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: dependency quantified Boolean formulas; DQBF; binary decision diagrams; BDD; DQBDD
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 5. 2022 14:57.
    3. CHALUPA, Marek, David KLAŠKA, Jan STREJČEK a Lukáš TOMOVIČ. Fast Computation of Strong Control Dependencies. In Alexandra Silva, K. Rustan M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2021, s. 887-910. ISBN 978-3-030-81687-2. Dostupné z: https://dx.doi.org/10.1007/978-3-030-81688-9_41.
      URL
      RIV/00216224:14330/21:00121991 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, domácí) -- Klaška, David (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Tomovič, Lukáš (703 Slovensko, domácí)
      Klíčová slova anglicky: control dependence;non-termination sensitive control dependence;decisive order dependence;control closure;ntscd;dod;graph theory
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 5. 2022 14:53.
    4. CHALUPA, Marek, Tomáš JAŠEK, Jakub NOVÁK, Anna ŘECHTÁČKOVÁ, Veronika ŠOKOVÁ a Jan STREJČEK. Symbiotic 8: Beyond Symbolic Execution. In Jan Friso Groote, Kim Guldstrand Larsen. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2021, s. 453-457. ISBN 978-3-030-72012-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-72013-1_31.
      URL
      RIV/00216224:14330/21:00121992 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, garant, domácí) -- Jašek, Tomáš (703 Slovensko, domácí) -- Novák, Jakub (703 Slovensko, domácí) -- Řechtáčková, Anna (203 Česká republika, domácí) -- Šoková, Veronika (703 Slovensko) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution;k-induction;program slicing;symbiotic;predator;klee
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 15. 5. 2024 02:10.
    5. CHALUPA, Marek, Jakub NOVÁK a Jan STREJČEK. Symbiotic 8: Parallel and Targeted Test Generation. In Esther Guerra and Mariëlle Stoelinga. Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 368-372. ISBN 978-3-030-71499-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-71500-7_20.
      URL
      RIV/00216224:14330/21:00121274 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, garant, domácí) -- Novák, Jakub (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: test generation; test coverage; Symbiotic
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 5. 2022 14:27.
    6. CHALUPA, Marek, Martina VITOVSKÁ, Tomáš JAŠEK, Michael ŠIMÁČEK a Jan STREJČEK. Symbiotic 6: generating test cases by slicing and symbolic execution. International Journal on Software Tools for Technology Transfer. 2021, roč. 23, č. 6, s. 875-877. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-020-00573-0.
      URL
      RIV/00216224:14330/21:00118732 Článek v odborném periodiku. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Vitovská, Martina (203 Česká republika, domácí) -- Jašek, Tomáš (703 Slovensko, domácí) -- Šimáček, Michael (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic;Program Slicing;Symbolic execution;KLEE
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 4. 2022 01:11.
    7. Symbiotic 8 (software)
      CHALUPA, Marek, Tomáš JAŠEK, Jakub NOVÁK, Anna ŘECHTÁČKOVÁ, Veronika ŠOKOVÁ a Jan STREJČEK. Symbiotic 8. 2021.
      Odkaz na stránku software
      RIV/00216224:14330/21:00119972 Software. angličtina. Česká republika.
      Chalupa, Marek (203 Česká republika, domácí) -- Jašek, Tomáš (703 Slovensko, domácí) -- Novák, Jakub (703 Slovensko, domácí) -- Řechtáčková, Anna (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic; symbolic execution; slicing; bug-finding
      Mezinárodní význam: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 6. 11. 2023 10:41.

    2020

    1. CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking Revisited. International Journal on Software Tools for Technology Transfer (STTT). Springer, 2020, roč. 22, č. 2, s. 115-133. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-019-00526-2.
      URL
      RIV/00216224:14330/20:00113978 Článek v odborném periodiku. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Vitovská, Martina (203 Česká republika, domácí)
      Klíčová slova anglicky: memory safety; instrumentation; program slicing; symbolic execution; Symbiotic
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 07:54.
    2. BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. Theoretical Computer Science. AMSTERDAM: North Holland, 2020, roč. 840, Nov 2020, s. 122-142. ISSN 0304-3975. Dostupné z: https://dx.doi.org/10.1016/j.tcs.2020.07.015.
      URL
      RIV/00216224:14330/20:00114391 Článek v odborném periodiku. angličtina. Nizozemské království.
      Blahoudek, František (203 Česká republika) -- Major, Juraj (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: LTL; Omega-automata; LTL to automata translation; Alternating automata; ltl3tela
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 12:31.
    3. BLAHOUDEK, František, Alexandre DURET-LUTZ a Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Cham (Switzerland): Springer, 2020, s. 15-27. ISBN 978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8_2.
      URL
      RIV/00216224:14330/20:00114393 Stať ve sborníku. angličtina. Švýcarsko.
      Blahoudek, František (203 Česká republika) -- Duret-Lutz, Alexandre (250 Francie) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: semi-determinization; complementation; generalized Büchi automata; Seminator

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 08:10.
    4. JONÁŠ, Martin a Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Cham (Switzerland): Springer, 2020, s. 378-393. ISBN 978-3-030-51824-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-51825-7_27.
      URL
      RIV/00216224:14330/20:00114392 Stať ve sborníku. angličtina. Švýcarsko.
      Jonáš, Martin (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: SMT solving; bit-vector logic; Boolector; Q3B
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 12:29.
    5. CHALUPA, Marek, Tomáš JAŠEK, Lukáš TOMOVIČ, Martin HRUŠKA, Veronika ŠOKOVÁ, Paulína AYAZIOVÁ, Jan STREJČEK a Tomáš VOJNAR. Symbiotic 7: Integration of Predator and More (Competition Contribution). In Armin Biere, David Parker. Tools and Algorithms for the Construction and Analysis of Systems. Německo: Springer, 2020, s. 413-417. ISBN 978-3-030-45236-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-45237-7_31.
      URL
      Název anglicky: Symbiotic 7: Integration of Predator and More (Competition Contribution)
      RIV/00216224:14330/20:00114113 Stať ve sborníku. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, garant, domácí) -- Jašek, Tomáš (703 Slovensko, domácí) -- Tomovič, Lukáš (703 Slovensko, domácí) -- Ayaziová, Paulína (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Vojnar, Tomáš (203 Česká republika)
      Klíčová slova anglicky: Symbiotic;Predator;Program Slicing;Termination Analysis;Shape Analysis;Symbolic Execution
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 12:25.

    2019

    1. CHALUPA, Marek a Jan STREJČEK. Evaluation of Program Slicing in Software Verification. In Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa. Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 101-119. ISBN 978-3-030-34967-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-34968-4_6.
      URL
      RIV/00216224:14330/19:00107773 Stať ve sborníku. angličtina. Švýcarsko.
      Chalupa, Marek (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: program analysis; static program slicing; verification
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 8. 1. 2020 10:45.
    2. BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER a 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, s. 445-461. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_26.
      URL
      RIV/00216224:14330/19:00107786 Stať ve sborníku. angličtina. Švýcarsko.
      Baier, Christel (276 Německo) -- Blahoudek, František (203 Česká republika) -- Duret-Lutz, Alexandre (756 Švýcarsko) -- Klein, Joachim (276 Německo) -- Müller, David (276 Německo) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: TELA; Emerson-Lei automata; emptiness check; probabilistic model checking
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 11:04.
    3. BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 152-171. ISBN 978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3_10.
      URL
      RIV/00216224:14330/19:00107795 Stať ve sborníku. angličtina. Švýcarsko.
      Blahoudek, František (203 Česká republika) -- Major, Juraj (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 00:00.
    4. MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ a 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, s. 357-365. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_21.
      URL
      RIV/00216224:14330/19:00107770 Stať ve sborníku. angličtina. Švýcarsko.
      Major, Juraj (703 Slovensko, domácí) -- Blahoudek, František (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Jánošová, Miriama (703 Slovensko, domácí) -- Zbončáková, Tatiana (703 Slovensko, domácí)
      Klíčová slova anglicky: ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 00:04.
    5. JONÁŠ, Martin a Jan STREJČEK. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. Online. In Isil Dillig, Serdar Tasiran. CAV 2019: Computer Aided Verification. Cham (Switzerland): Springer, 2019, s. 64-73. ISBN 978-3-030-25542-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-25543-5_4.
      URL
      RIV/00216224:14330/19:00107610 Stať ve sborníku. angličtina. Švýcarsko.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: satisfiability; satisfiability modulo theories; bit-vectors; quantifiers; tool
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2020 07:44.

    2018

    1. JONÁŠ, Martin a Jan STREJČEK. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018, s. 273-291. ISBN 978-3-030-02507-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02508-3_15.
      URL
      RIV/00216224:14330/18:00101330 Stať ve sborníku. angličtina. Švýcarsko.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: satisfiability modulo theories; binary decision diagrams; abstractions; bit-vectors
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2019 15:23.
    2. JONÁŠ, Martin a Jan STREJČEK. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?. Online. In Gilles Barthe, Geoff Sutcliffe, Margus Veanes. LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Neuveden: EasyChair, 2018, s. 488-497. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/spnx.
      URL
      RIV/00216224:14330/18:00101333 Stať ve sborníku. angličtina. Velká Británie a Severní Irsko.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: satisfiability modulo theories; quantified bit-vectors; bit-width; experimental evaluation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 31. 5. 2022 14:22.
    3. CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking. In María-del-Mar Gallardo and Pedro Merino. Model Checking Software. SPIN 2018. Cham, Švýcarsko: Springer, 2018, s. 115-132. ISBN 978-3-319-94110-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-94111-0_7.
      RIV/00216224:14330/18:00101043 Stať ve sborníku. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Vitovská, Martina (203 Česká republika, domácí)
      Klíčová slova anglicky: program analysis; program verification; memory safety
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2019 15:39.
    4. JONÁŠ, Martin a Jan STREJČEK. On the complexity of the quantified bit-vector arithmetic with binary encoding. Information Processing Letters. Elsevier, 2018, roč. 135, červenec 2018, s. 57-61. ISSN 0020-0190. Dostupné z: https://dx.doi.org/10.1016/j.ipl.2018.02.018.
      URL
      RIV/00216224:14330/18:00100916 Článek v odborném periodiku. angličtina. Nizozemské království.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: computational complexity; satisfiability modulo theories; bit-vector theory
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2019 15:54.
    5. CHALUPA, Marek, Martina VITOVSKÁ a Jan STREJČEK. Symbiotic 5: Boosted Instrumentation (Competition Contribution). In Dirk Beyer and Marieke Huisman. Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, Proceedings, Part II. Berlin: Springer, 2018, s. 442-446. ISBN 978-3-319-89963-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-89963-3_29.
      RIV/00216224:14330/18:00100910 Stať ve sborníku. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Vitovská, Martina (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic; program analysis; program verification; SV-COMP 2018
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 28. 9. 2019 14:33.

    2017

    1. JONÁŠ, Martin a Jan STREJČEK. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In Serge Gaspers, Toby Walsh. Theory and Applications of Satisfiability Testing – SAT 2017. Cham (Switzerland): Springer, 2017, s. 364-379. ISBN 978-3-319-66262-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-66263-3_23.
      URL
      RIV/00216224:14330/17:00095125 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: SMT solving; formula simplifications; bit-vectors
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 14. 5. 2020 15:12.
    2. BLAHOUDEK, František, Alexandre DURET-LUTZ, Mikuláš KLOKOČKA, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Seminator: A Tool for Semi-Determinization of Omega-Automata. Online. In Thomas Eiter and David Sands. Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017). Neuveden: EasyChair, 2017, s. 356-367. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/k5nl.
      URL
      RIV/00216224:14330/17:00094743 Stať ve sborníku. Informatika. angličtina. Německo.
      Blahoudek, František (203 Česká republika, domácí) -- Duret-Lutz, Alexandre (250 Francie) -- Klokočka, Mikuláš (203 Česká republika, domácí) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: semi deterministic automata; ltl to automata translation; omega automata
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 9. 11. 2018 14:58.
    3. CHALUPA, Marek, Martina VITOVSKÁ, Martin JONÁŠ, Jiří SLABÝ a Jan STREJČEK. Symbiotic 4: Beyond Reachability (Competition Contribution). In Axel Legay, Tiziana Margaria. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference. Berlin: Springer Berlin Heidelberg, 2017, s. 385-389. ISBN 978-3-662-54580-5. Dostupné z: https://dx.doi.org/10.1007/978-3-662-54580-5_28.
      URL
      RIV/00216224:14330/17:00095057 Stať ve sborníku. Informatika. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Vitovská, Martina (203 Česká republika, domácí) -- Jonáš, Martin (203 Česká republika, domácí) -- Slabý, Jiří (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbiotic; program analysis; program verification; SV-COMP 2017
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:22.

    2016

    1. BLAHOUDEK, František, Matthias HEIZMANN, Sven SCHEWE, Jan STREJČEK a Ming-Hsien TSAI. Complementing Semi-deterministic Büchi Automata. In Marsha Chechik, Jean-François Raskin. Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016. Berlin: Springer Berlin Heidelberg, 2016, s. 770-787. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_49.
      URL
      RIV/00216224:14330/16:00088081 Stať ve sborníku. Informatika. angličtina. Německo.
      Blahoudek, František (203 Česká republika, domácí) -- Heizmann, Matthias (276 Německo) -- Schewe, Sven (276 Německo) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Tsai, Ming-Hsien (158 Tchaj-wan)
      Klíčová slova anglicky: Buchi automata;complementation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 23:01.
    2. BOUDA, Jan, Lukáš HOLÍK, Jan KOFROŇ, Jan STREJČEK a Adam RAMBOUSEK. MEMICS 2016. 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 1., elektronické vyd. Brno: Masarykova univerzita, 2016. ISBN 978-80-210-8362-2.
      Čítárna Munispace
      Název česky: MEMICS 2016
      Název anglicky: MEMICS 2016. 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
      Informatika. angličtina. Česká republika.
      Změnila: Mgr. Radka Vyskočilová, učo 2368. Změněno: 8. 11. 2016 09:10.
    3. JONÁŠ, Martin a Jan STREJČEK. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Nadia Creignou and Daniel Le Berre. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference. Berlin, Heidelberg: Springer, 2016, s. 267-283. ISBN 978-3-319-40969-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-40970-2_17.
      RIV/00216224:14330/16:00088245 Stať ve sborníku. Informatika. angličtina. Německo.
      Jonáš, Martin (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: SMT solving; quantified bit-vector formulas; BDD
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:22.
    4. CHALUPA, Marek, Martin JONÁŠ, Jiří SLABÝ, Jan STREJČEK a Martina VITOVSKÁ. Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution). In Marsha Chechik and Jean-Francois Raskin. Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin, Heidelberg: Springer, 2016, s. 946-949. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_67.
      RIV/00216224:14330/16:00088244 Stať ve sborníku. Informatika. angličtina. Německo.
      Chalupa, Marek (203 Česká republika, domácí) -- Jonáš, Martin (203 Česká republika, domácí) -- Slabý, Jiří (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Vitovská, Martina (203 Česká republika, domácí)
      Klíčová slova anglicky: instrumentation; symbolic execution; program slicing
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:22.
    5. ČADEK, Pavel, Jan STREJČEK a Marek TRTÍK. Tighter Loop Bound Analysis. In Cyrille Artho and Axel Legay and Doron Peled. Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Berlin, Heidelberg: Springer, 2016, s. 512-527. ISBN 978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3_32.
      RIV/00216224:14330/16:00088246 Stať ve sborníku. Informatika. angličtina. Německo.
      Čadek, Pavel (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika)
      Klíčová slova anglicky: loop bounds; symbolic execution
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:27.

    2015

    1. BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR a 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, s. 66-83. ISBN 978-3-319-23403-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-23404-5_6.
      Název česky: O zpřesňování Büchiho automatů pro explicitní metodu ověřování modelu.
      RIV/00216224:14330/15:00080986 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Blahoudek, František (203 Česká republika, domácí) -- Duret-Lutz, Alexandre (250 Francie) -- Rujbr, Vojtěch (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: linear temporal logic; Büchi automata; explicit model checking; specification refinement
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 20:47.
    2. BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER a Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, s. 479-486. ISBN 978-3-319-21689-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-21690-4_31.
      RIV/00216224:14330/15:00080919 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Babiak, Tomáš (703 Slovensko, domácí) -- Blahoudek, František (203 Česká republika, domácí) -- Duret-Lutz, Alexandre (250 Francie) -- Klein, Joachim (276 Německo) -- Křetínský, Jan (203 Česká republika, garant, domácí) -- Müller, David (276 Německo) -- Parker, David (826 Velká Británie a Severní Irsko) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: automata; infinite words; verification
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2016 14:24.

    2014

    1. BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a 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, s. 68-76. ISBN 978-1-4503-2452-6. Dostupné z: https://dx.doi.org/10.1145/2632362.2632377.
      Název česky: Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
      RIV/00216224:14330/14:00073815 Stať ve sborníku. Informatika. angličtina. Spojené státy.
      Blahoudek, František (203 Česká republika, domácí) -- Duret-Lutz, Alexandre (250 Francie) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: linear temporal logic; Büchi automata; explicit model checking
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 11. 7. 2019 13:31.
    2. SLABÝ, Jiří a Jan STREJČEK. Symbiotic 2: More Precise Slicing (Competition Contribution). In E. Ábrahám and K. Havelund. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014. Berlin, Heidelberg: Springer, 2014, s. 415-417. ISBN 978-3-642-54861-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-54862-8_34.
      RIV/00216224:14330/14:00073504 Stať ve sborníku. Informatika. angličtina. Německo.
      Slabý, Jiří (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: instrumentation; symbolic execution; program slicing
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2015 05:35.
    3. TRTÍK, Marek a Jan STREJČEK. Symbolic Memory with Pointers. In Franck Cassez and Jean-Francois Raskin. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Berlin Heidelberg: Springer, 2014, s. 380-395. ISBN 978-3-319-11935-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-11936-6_27.
      Název česky: Symbolická paměť s ukazateli
      RIV/00216224:14330/14:00074092 Stať ve sborníku. Informatika. angličtina. Německo.
      Trtík, Marek (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: symbolic execution; symbolic memory
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 13. 11. 2014 16:23.

    2013

    1. SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. ClabureDB: Classified Bug-Reports Database Tool for Developers of Program Analysis Tools. In Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni. Verification, Model Checking, and Abstract Interpretation: 14th International Conference, VMCAI 2013. Berlin, Heidelberg: Springer, 2013, s. 268-274. ISBN 978-3-642-35872-2. Dostupné z: https://dx.doi.org/10.1007/978-3-642-35873-9_17.
      RIV/00216224:14330/13:00065952 Stať ve sborníku. Informatika. angličtina. Německo.
      Slabý, Jiří (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: Bug database; classified bug-reports
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 17. 4. 2014 11:19.
    2. SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Compact Symbolic Execution. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 193-207. ISBN 978-3-319-02443-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-02444-8_15.
      Název česky: Kompaktní symbolická exekuce
      RIV/00216224:14330/13:00066165 Stať ve sborníku. Informatika. angličtina. Německo.
      Slabý, Jiří (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution; compact symbolic execution; testing
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 18. 11. 2013 14:45.
    3. BLAHOUDEK, František, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Comparison of LTL to Deterministic Rabin Automata Translators. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov. Logic for Programming Artificial Intelligence and Reasoning, LPAR-19. Berlin Heidelberg: Springer, 2013, s. 164-172. ISBN 978-3-642-45220-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-45221-5_12.
      Název česky: Srovnání překladačů LTL na deterministické Rabinovy automaty
      RIV/00216224:14330/13:00066512 Stať ve sborníku. Informatika. angličtina. Německo.
      Blahoudek, František (203 Česká republika, domácí) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: linear temporal logic; deterministic omega-automata; LTL3DRA; Rabinizer; ltl2dstar
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 3. 6. 2014 11:26.
    4. BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a 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, s. 81-98. ISBN 978-3-642-39175-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39176-7_6.
      RIV/00216224:14330/13:00066141 Stať ve sborníku. Informatika. angličtina. Spojené státy.
      Babiak, Tomáš (703 Slovensko, domácí) -- Badie, Thomas (250 Francie) -- Duret-Lutz, Alexandre (250 Francie) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: linear time logic; model-checking; translation LTL to Buchi automata
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 15. 11. 2013 23:28.
    5. BLAHOUDEK, František, Tomáš BABIAK, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 24-38. ISBN 978-3-319-02443-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-02444-8_4.
      Název česky: Efektivní překlad LTL na deterministické Rabinovy automaty
      RIV/00216224:14330/13:00066175 Stať ve sborníku. Informatika. angličtina. Spojené státy.
      Blahoudek, František (203 Česká republika, domácí) -- Babiak, Tomáš (703 Slovensko, domácí) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: linear temporal logic; deterministic omega-automata
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 15. 11. 2013 23:58.
    6. SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). In Nir Piterman, Scott A. Smolka. Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Berlin, Heidelberg: Springer, 2013, s. 630-632. ISBN 978-3-642-36741-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-36742-7_50.
      RIV/00216224:14330/13:00065969 Stať ve sborníku. Informatika. angličtina. Německo.
      Slabý, Jiří (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: instrumentation; symbolic execution; program slicing
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2014 22:59.

    2012

    1. STREJČEK, Jan a Marek TRTÍK. Abstracting Path Conditions. In Mats Per Erik Heimdahl, Zhendong Su. Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012. New York, NY, USA: ACM, 2012, s. 155-165. ISBN 978-1-4503-1454-1. Dostupné z: https://dx.doi.org/10.1145/2338965.2336772.
      URL
      RIV/00216224:14330/12:00057592 Stať ve sborníku. Informatika. angličtina. Česká republika.
      Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: Symbolic execution; Path conditions; Program location reachability; Tests generation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 7. 1. 2016 22:12.
    2. BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science. Cambridge: Cambridge University Press, 2012, roč. 22, č. 2, s. 203-235. ISSN 0960-1295. Dostupné z: https://dx.doi.org/10.1017/S0960129511000399.
      URL
      Název česky: Skoro lineární Büchiho automaty
      Název anglicky: Almost linear Büchi automata
      RIV/00216224:14330/12:00057181 Článek v odborném periodiku. Informatika. angličtina. Česká republika.
      Babiak, Tomáš (703 Slovensko, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Řehák, Vojtěch (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: LTL; linear time logic; model checking
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 22. 4. 2013 05:15.
    3. ClabureDB (software)
      SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. ClabureDB. 2012.
      ClabureDB
      RIV/00216224:14330/12:00062341 Software. Informatika. angličtina. Česká republika.
      Slabý, Jiří (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: Bug database; classified bug-reports

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 4. 2013 05:57.
    4. SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012. Berlin, Heidelberg: Springer, 2012, s. 207-221. ISBN 978-3-642-32468-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-32469-7_14.
      URL
      RIV/00216224:14330/12:00057431 Stať ve sborníku. Informatika. angličtina. Německo.
      Slabý, Jiří (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, garant, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: Bug finding; Symbolic execution; Program slicing; FSM property specification; Code instrumentation
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: Mgr. Jiří Slabý, Ph.D., učo 98734. Změněno: 20. 1. 2013 11:34.
    5. BABIAK, Tomáš, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012, s. 95-109. ISBN 978-3-642-28755-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-28756-5_8.
      URL
      Název česky: Překlad LTL na Büchiho automaty: rychle a determinističtěji
      RIV/00216224:14330/12:00057222 Stať ve sborníku. Informatika. angličtina. Německo.
      Babiak, Tomáš (203 Česká republika, garant, domácí) -- Křetínský, Mojmír (203 Česká republika, domácí) -- Řehák, Vojtěch (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: Linear Temporal Logic; Büchi Automata
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 9. 4. 2013 18:14.
    6. Symbiotic (software)
      SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Symbiotic. 2012.
      Odkaz na stránku software
      RIV/00216224:14330/12:00062340 Software. Informatika. angličtina. Česká republika.
      Slabý, Jiří (203 Česká republika, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Trtík, Marek (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution; slicing; bug-finding
      Mezinárodní význam: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 4. 2013 05:58.

    2010

    1. BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost Linear Büchi Automata. In MEMICS 2010. 2010. ISBN 978-80-87342-10-7.
      Název česky: Skoro lineární Büchiho automaty
      Název anglicky: Almost Linear Büchi Automata
      RIV/00216224:14330/10:00045184 Prezentace na konferencích. Informatika. angličtina. Česká republika.
      Babiak, Tomáš (703 Slovensko, garant, domácí) -- Strejček, Jan (203 Česká republika, domácí) -- Řehák, Vojtěch (203 Česká republika, domácí)
      Klíčová slova anglicky: LTL; linear time logic; Büchi Automata; model checking
      Druh účasti: aktivní účast

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 11. 1. 2011 16:52.
    2. ŘEHÁK, Vojtěch, Petr SLOVÁK, Jan STREJČEK a Loïc HÉLOUËT. Decidable Race Condition and Open Coregions in HMSC. In Jochen Küster, Emilio Tuosto. Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010). Paphos, Kypr: ECEASST, 2010, 12 s. ISSN 1863-2122.
      URL
      Název česky: Rozhodnutelné podmínky souběhu a otevřené koregiony v HMSC
      RIV/00216224:14330/10:00043646 Stať ve sborníku. Informatika. angličtina. Kypr.
      Řehák, Vojtěch (203 Česká republika, garant, domácí) -- Slovák, Petr (203 Česká republika) -- Strejček, Jan (203 Česká republika, domácí) -- Hélouët, Loïc (250 Francie)
      Klíčová slova anglicky: HMSC; race condition; trace-race condition; open coregions;
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 28. 4. 2011 15:15.
    3. STREJČEK, Jan. Young Researchers Forum. 2010.
      URL
      Název česky: Fórum mladých výzkumníků
      Teorie informace. angličtina. Česká republika.
      Klíčová slova anglicky: theoretical computer science

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 20. 8. 2010 13:20.

    2009

    1. BABIAK, Tomáš, Vojtěch ŘEHÁK a 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, s. 16-25. ISSN 2075-2180.
      DOI
      Název česky: Skoro lineární Büchiho automaty
      RIV/00216224:14330/09:00029631 Stať ve sborníku. Informatika. angličtina. Itálie.
      Babiak, Tomáš (703 Slovensko) -- Řehák, Vojtěch (203 Česká republika, garant) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: LTL; linear time logic; model checking
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 23. 11. 2009 16:12.
    2. BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica. Berlin: Springer-Verlag, 2009, roč. 46, č. 1, s. 1-28. ISSN 0001-5903.
      URL
      Název česky: O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy
      RIV/00216224:14330/09:00029078 Článek v odborném periodiku. Informatika. angličtina. Německo.
      Bozzelli, Laura (380 Itálie) -- Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: infinite-state systems; linear time logic; decidability; model checking
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 22. 5. 2009 16:43.
    3. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a 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). 2009. vyd. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009, s. 105-117. ISSN 1571-0661.
      URL
      Název česky: O rozhodnutelnosti ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
      RIV/00216224:14330/09:00028439 Stať ve sborníku. Informatika. angličtina. Portugalsko.
      Křetínský, Mojmír (203 Česká republika) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: process rewrite systems; LTL; infinite-state; model-checking; decidability
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 23. 6. 2009 16:57.
    4. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Reachability is decidable for weakly extended process rewrite systems. Information and Computation. Elsevier, 2009, roč. 207, č. 6, s. 671-680. ISSN 0890-5401.
      URL
      Název česky: Dosažitelnost je rozhodnutelná pro slabě rozšířené procesové přepisovací systémy
      RIV/00216224:14330/09:00028490 Článek v odborném periodiku. Informatika. angličtina. Německo.
      Křetínský, Mojmír (203 Česká republika) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; (un)decidability; reachability
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 7. 5. 2009 10:19.

    2008

    1. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science. Amsterdam, North Holland: Elsevier Science Publishers, 2008, roč. 394, 1-2, s. 134-140. ISSN 0304-3975.
      Název česky: Petriho sítě mají menší vyjadřovací sílu než stavově-rozšířené PA
      RIV/00216224:14330/08:00024164 Článek v odborném periodiku. Informatika. angličtina. Nizozemské království.
      Křetínský, Mojmír (203 Česká republika) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: Petri nets; PA processes; bisimulation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 22. 5. 2009 16:55.

    2007

    1. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a 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.
      Název česky: Rozhodnutelnost ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
      RIV/00216224:14330/07:00019467 Prezentace na konferencích. Informatika. angličtina. Portugalsko.
      Křetínský, Mojmír (203 Česká republika, garant, domácí) -- Řehák, Vojtěch (203 Česká republika, domácí) -- Strejček, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: process rewrite systems; LTL; infinite-state; model-checking; decidability
      Druh sborníku: předkonferenční sborník
      Druh účasti: aktivní účast
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 28. 4. 2011 14:50.
    2. BOUAJJANI, Ahmed, Jan STREJČEK a 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, s. 47-64. ISSN 1571-0661.
      URL
      Název česky: Symbolicka verifikace slabe rozsirenych PAD
      RIV/00216224:14330/07:00021744 Stať ve sborníku. Informatika. angličtina. Německo.
      Bouajjani, Ahmed (504 Maroko) -- Strejček, Jan (203 Česká republika, garant) -- Touili, Tayssir (788 Tunisko)
      Klíčová slova anglicky: rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 6. 2009 17:48.

    2006

    1. BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a 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, s. 248-259. ISBN 978-3-540-49994-7.
      Název česky: O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy
      RIV/00216224:14330/06:00015417 Stať ve sborníku. Informatika. angličtina. Indie.
      Bozzelli, Laura (380 Itálie) -- Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: infinite-state systems; linear time logic; decidability; model checking
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 20. 12. 2011 18:12.
    2. BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Brno: FI MU, 2006. FIMU-RS-2006-05.
      URL
      Název česky: O rozhodnutelnosti problému ověřování modelu pro LTL a slabě royšířené procesové přepisovací systémy
      RIV/00216224:14330/06:00015439 Audiovizuální tvorba. Informatika. angličtina. Česká republika.
      Bozzelli, Laura (380 Itálie) -- Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: infinite-state systems; linear time logic; decidability; model checking
      Mezinárodní význam: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 31. 3. 2010 15:19.
    3. BOUAJJANI, Ahmed, Jan STREJČEK a 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, s. 29-41.
      Název česky: Symbolicka verifikace slabe rozsirenych PAD
      RIV/00216224:14330/06:00018747 Stať ve sborníku. Informatika. angličtina. Německo.
      Bouajjani, Ahmed (504 Maroko) -- Strejček, Jan (203 Česká republika, garant) -- Touili, Tayssir (788 Tunisko)
      Klíčová slova anglicky: rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 18. 6. 2007 14:11.
    4. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05). 2006. vyd. Amsterdam, The Netherlands: Elsevier Science, 2006, s. 17-36. ISSN 1571-0661.
      URL
      Název česky: Zjemneni hranice nerozhodnutelnosti slabe bisimulace
      Název anglicky: Refining Undecidability Border of Weak Bisimilarity
      RIV/00216224:14330/06:00015292 Stať ve sborníku. Informatika. angličtina. Nizozemské království.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; decidability; weak bisimilarity
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 23. 6. 2009 16:53.

    2005

    1. PELÁNEK, Radek a Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005, s. 238-249. ISBN 978-3-540-31023-5.
      Název česky: Hlubší spojitosti mezi LTL a alternujícími automaty
      RIV/00216224:14330/05:00012729 Stať ve sborníku. Informatika. angličtina. Francie.
      Pelánek, Radek (203 Česká republika) -- Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: LTL; alternating automata; model checking
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 29. 3. 2010 12:50.
    2. KUČERA, Antonín a 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, s. 239-249. ISBN 3-540-24302-X.
      Název česky: Charakteristické vzorce pro LTL
      RIV/00216224:14330/05:00012348 Stať ve sborníku. Informatika. angličtina. Slovensko.
      Kučera, Antonín (203 Česká republika, garant) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: model-checking; linear temporal logic
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 29. 3. 2010 14:38.
    3. STREJČEK, Jan. Linear Temporal Logic: Expressiveness and Model Checking. Faculty of Informatics, Masaryk University, 2005, 148 s.
      Název česky: Lineární temporální logika: vyjadřovací síla a metoda ověřování modelu
      Informatika. angličtina. Česká republika.
      Klíčová slova anglicky: Linear temporal logic, expressiveness, model checking, stuttering, Thesis

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 3. 1. 2007 17:02.
    4. BOUAJJANI, Ahmed, Javier ESPARZA, Stefan SCHWOON a Jan STREJČEK. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 348-359. ISBN 3-540-30495-9.
      Název česky: Analýza dosažitelnosti pro vícevláknové programy s asynchronní komunikací
      RIV/00216224:14330/05:00012714 Stať ve sborníku. Informatika. angličtina. Německo.
      Bouajjani, Ahmed (250 Francie) -- Esparza, Javier (724 Španělsko) -- Schwoon, Stefan (276 Německo) -- Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: bounded reachability; symbolic reachability; asynchronous dynamic pushdown network
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 29. 3. 2010 14:27.
    5. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 213-224. ISBN 3-540-30495-9.
      Název česky: Dosažitelnost Hennessy-Milner vlastností pro slabě rozšířené PRS
      RIV/00216224:14330/05:00012582 Stať ve sborníku. Informatika. angličtina. Německo.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 8. 4. 2010 21:40.
    6. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. BRICS Notes Series. San Francisco, USA, 2005, roč. 2005, NS-05-4, s. 3-14. ISSN 0909-3206.
      URL
      Název česky: Zjemneni hranice nerozhodnutelnosti pro slabou bisimulaci
      RIV/00216224:14330/05:00012580 Článek v odborném periodiku. Informatika. angličtina. Česká republika.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; (un)decidability; weak bisimulation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 4. 12. 2006 16:38.
    7. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper). Brno: FI MU, 2005. FIMU-RS-2005-06.
      URL
      Název česky: Zjemneni hranice nerozhodnutelnosti pro slabou bisimulaci
      RIV/00216224:14330/05:00012581 Audiovizuální tvorba. Informatika. angličtina. Česká republika.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; (un)decidability; weak bisimulation
      Mezinárodní význam: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 27. 11. 2006 15:12.
    8. KUČERA, Antonín a Jan STREJČEK. The stuttering principle revisited. Acta informatica. Berlin: Springer-Verlag, 2005, roč. 41, 7/8, s. 415-434. ISSN 0001-5903.
      Název česky: Znovu o principu periodických vzorů
      RIV/00216224:14330/05:00012554 Článek v odborném periodiku. Informatika. angličtina. Německo.
      Kučera, Antonín (203 Česká republika, garant) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: linear temporal logic; stuttering
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 27. 11. 2006 15:12.

    2004

    1. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Extended Process Rewrite Systems: Expressiveness and Reachability. In CONCUR 2004 - Concurrency Theory. LNCS 3170. Berlin, Heidelberg, New York: Springer, 2004, s. 355-370. ISBN 3-540-22940-X.
      Název česky: Rozšířené procesové přepisovací systémy: Vyjadřovací síla a dosažitelnost
      RIV/00216224:14330/04:00010262 Stať ve sborníku. Informatika. angličtina. Velká Británie a Severní Irsko.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; expressivness; reachability; decidability
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 11. 3. 2010 13:41.
    2. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems. 2004. vyd. Amsterdam, The Netherlands: Elsevier Science, 2004, s. 75-88. ISSN 1571-0661.
      URL
      Název česky: O rozšířených procesových přepisovacích systémech: Přepisovací systémy se slabou konečně stavovou jednotkou
      RIV/00216224:14330/04:00010392 Stať ve sborníku. Informatika. angličtina. Nizozemské království.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; decidability; reachability
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 6. 2009 17:11.
    3. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On the Expressive Power of Extended Process Rewrite Systems. BRICS Report Series. Aarhus: Basic Research in Computer Science, 2004, roč. 2004, RS-04-7, s. 1-18. ISSN 0909-0878.
      URL
      Název česky: O vyjadřovací síle rozšířených procesových přepisovacích systémů
      RIV/00216224:14330/04:00010025 Článek v odborném periodiku. Informatika. angličtina. Česká republika.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state; expressivness; reachability

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 24. 1. 2005 17:02.

    2003

    1. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Prelim.Proc.of the 5th Internat.Workshop on Verification of Infinite-State Systems (INFINITY'2003). Marseille, France: Universite de Provence, Marseille, 2003, s. 73-86.
      RIV/00216224:14330/03:00008151 Stať ve sborníku. Informatika. angličtina. Francie.
      Křetínský, Mojmír (203 Česká republika, garant) -- Řehák, Vojtěch (203 Česká republika) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state
      Recenzováno: ano

      Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 16. 11. 2006 12:47.
    2. KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Process Rewrite Systems with Weak Finite-State Unit (full version of INFINITY'2003 paper). Brno: FI MU, 2003, 23 s. FIMU-RS-2003-05.
      Informatika. angličtina. Česká republika.
      Klíčová slova anglicky: process rewrite systems; state extension; infinite-state

      Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 24. 5. 2006 15:51.

    2002

    1. STREJČEK, Jan. Boundaries and Efficiency of Verification. In Proceedings of summer school MOVEP 2002. Nantes (France): IRCCyN, Ecole Centrale de Nantes, France, 2002, s. 403-408.
      RIV/00216224:14330/02:00006434 Stať ve sborníku. Počítačový hardware a software. angličtina. Francie.
      Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: stuttering; constrained rewrite systems
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 27. 11. 2006 15:12.
    2. KUČERA, Antonín a Jan STREJČEK. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. J. Bradfield (Ed.). In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin: Springer, 2002, s. 276-291. ISBN 3-540-44240-5.
      RIV/00216224:14330/02:00006381 Stať ve sborníku. Počítačový hardware a software. angličtina. Německo.
      Kučera, Antonín (203 Česká republika, garant) -- Strejček, Jan (203 Česká republika)
      Klíčová slova anglicky: verification; concurrency; weak bisimilarity; infinite-state systems
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 20. 12. 2011 18:12.
      Přír. čísla: 4200508076
    3. CRHOVÁ, Jitka, Pavel KRČÁL, Jan STREJČEK, David ŠAFRÁNEK a Pavel ŠIMEČEK. YAHODA: verification tools database. In Proceedings of Tools Day. Brno: FI MU, 2002, s. 99-103.
      FI MU Report Series
      RIV/00216224:14330/02:00006433 Stať ve sborníku. Počítačový hardware a software. angličtina. Česká republika.
      Crhová, Jitka (203 Česká republika) -- Krčál, Pavel (203 Česká republika) -- Strejček, Jan (203 Česká republika) -- Šafránek, David (203 Česká republika, garant) -- Šimeček, Pavel (203 Česká republika)
      Klíčová slova anglicky: formal verification
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 27. 11. 2006 15:12.

    2001

    1. STREJČEK, Jan. Rewrite Systems with Constraints. In EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency. Aalborg (Denmark): Elsevier Science, 2001, s. 1-20.
      URL
      Název česky: Přepisovací systémy s omezeními
      Název anglicky: Rewrite Systems with Constraints
      RIV/00216224:14330/01:00004676 Stať ve sborníku. Počítačový hardware a software. angličtina. Nizozemské království.
      Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: (rewrite) transition system; concurrency; partial information; bisimulation equivalence; language expressibility

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 10. 1. 2005 15:31.

    2000

    1. STREJČEK, Jan. Constrained Rewrite Transition Systems. Brno: FI MU, 2000. Report Series, FIMU-RS-2000-12.
      URL URL
      Název česky: Přepisovací systémy s omezeními
      Název anglicky: Constrained Rewrite Transition Systems
      RIV/00216224:14330/00:00002662 Audiovizuální tvorba. Počítačový hardware a software. angličtina. Česká republika.
      Strejček, Jan (203 Česká republika, garant)
      Klíčová slova anglicky: (rewrite) transition system; concurrency; partial information; bisimulation equivalence; language expressibility

      Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 23. 6. 2009 17:08.
Zobrazeno: 19. 9. 2024 21:13