Masarykova univerzita

Výpis publikací

česky | in English

Filtrování publikací

    2021

    1. DIVINE 4.4 (software)
      ROČKAI, Petr, Henrich LAUKO, Vladimír ŠTILL, Zuzana BARANOVÁ, Lukáš KORENČIK, Adam MATOUŠEK, Jiří BARNAT, Jakub ŠÁRNÍK, Jan MRÁZEK, Katarína KEJSTOVÁ a Tadeáš KUČERA. DIVINE 4.4. 2021.
      URL zdrojový kód
      RIV/00216224:14330/21:00119996 Software. angličtina. Česká republika.
      Ročkai, Petr (703 Slovensko, garant, domácí) -- Lauko, Henrich (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Baranová, Zuzana (703 Slovensko) -- Korenčik, Lukáš (703 Slovensko) -- Matoušek, Adam (203 Česká republika) -- Barnat, Jiří (203 Česká republika) -- Šárník, Jakub (203 Česká republika) -- Mrázek, Jan (203 Česká republika) -- Kejstová, Katarína (703 Slovensko) -- Kučera, Tadeáš (203 Česká republika)
      Klíčová slova anglicky: model checking; correctness; analysis; concurrency; symbolic
      Mezinárodní význam: ano
      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 6. 11. 2023 10:42.
      Podrobněji: https://is.muni.cz/publication/1836137/cs

    2019

    1. Extending DIVINE with Symbolic Verification Using SMT
      LAUKO, Henrich, Vladimír ŠTILL, Petr ROČKAI a Jiří BARNAT. Extending DIVINE with Symbolic Verification Using SMT. In Beyer, Dirkand Huisman, Mariekeand Kordon, Fabriceand Steffen, Bernhard. Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing. s. 204-208. ISBN 978-3-030-17501-6. doi:10.1007/978-3-030-17502-3_14. 2019.
      URL
      RIV/00216224:14330/19:00107528 Stať ve sborníku. angličtina. Švýcarsko.
      Lauko, Henrich (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
      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:37.
      Podrobněji: https://is.muni.cz/publication/1547580/cs
    2. Local Nontermination Detection for Parallel C++ Programs
      ŠTILL, Vladimír a Jiří BARNAT. Local Nontermination Detection for Parallel C++ Programs. In Ölveczky P., Salaün G. International Conference on Software Engineering and Formal Methods. Cham: Springer. s. 373-390. ISBN 978-3-030-30445-4. doi:10.1007/978-3-030-30446-1_20. 2019.
      Author's page Publisher's page
      RIV/00216224:14330/19:00107759 Stať ve sborníku. angličtina. Švýcarsko.
      Štill, Vladimír (203 Česká republika, garant, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: termination; nontermination; local nontermination; parallel programs; c++; model checking; DIVINE
      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.
      Podrobněji: https://is.muni.cz/publication/1576677/cs

    2018

    1. DiVM: Model checking with LLVM and graph memory
      ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ a Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. Journal of Systems and Software. Elsevier, roč. 143, Oct, s. 1-13. ISSN 0164-1212. doi:10.1016/j.jss.2018.04.026. 2018.
      URL
      RIV/00216224:14330/18:00106878 Článek v odborném periodiku. angličtina. Nizozemské království.
      Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Černá, Ivana (203 Česká republika, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: Model checking; C plus; Virtual machine; Verification
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 5. 11. 2021 15:28.
      Podrobněji: https://is.muni.cz/publication/1528139/cs
    2. Model Checking of C++ Programs Under the x86-TSO Memory Model
      ŠTILL, Vladimír a Jiří BARNAT. Model Checking of C++ Programs Under the x86-TSO Memory Model. In Jing Sun, Meng Sun. Formal Methods and Software Engineering. Cham: Springer. s. 124-140. ISBN 978-3-030-02449-9. doi:10.1007/978-3-030-02450-5_8. 2018.
      Publisher's page Author's page
      RIV/00216224:14330/18:00101450 Stať ve sborníku. angličtina. Švýcarsko.
      Štill, Vladimír (203 Česká republika, garant, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: relaxed memory; model checking; c++; x86; memory model; DIVINE
      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: 30. 4. 2019 07:36.
      Podrobněji: https://is.muni.cz/publication/1479960/cs

    2017

    1. Model Checking of C and C++ with DIVINE 4
      BARANOVÁ, Zuzana, Jiří BARNAT, Katarína KEJSTOVÁ, Tadeáš KUČERA, Henrich LAUKO, Jan MRÁZEK, Petr ROČKAI a Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing. s. 201-207. ISBN 978-3-319-68166-5. doi:10.1007/978-3-319-68167-2_14. 2017.
      URL
      RIV/00216224:14330/17:00095126 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Baranová, Zuzana (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí) -- Kejstová, Katarína (703 Slovensko, domácí) -- Kučera, Tadeáš (203 Česká republika, domácí) -- Lauko, Henrich (703 Slovensko, domácí) -- Mrázek, Jan (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí)
      Klíčová slova anglicky: Model Checking; Verification; C; C++; DIVINE
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 10. 2018 16:24.
      Podrobněji: https://is.muni.cz/publication/1394153/cs
    2. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
      MRÁZEK, Jan, Martin JONÁŠ, Vladimír ŠTILL, Henrich LAUKO a Jiří BARNAT. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution). In Axel Legay, Tiziana Margaria. Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II. Berlin, Heidelberg: Springer. s. 390-393. ISBN 978-3-662-54579-9. doi:10.1007/978-3-662-54580-5_29. 2017.
      URL
      RIV/00216224:14330/17:00095131 Stať ve sborníku. Informatika. angličtina. Německo.
      Mrázek, Jan (203 Česká republika, domácí) -- Jonáš, Martin (203 Česká republika, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Lauko, Henrich (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: program verification; model checking; formula optimizations; caching
      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:23.
      Podrobněji: https://is.muni.cz/publication/1394228/cs
    3. Using Off-the-Shelf Exception Support Components in C++ Verification
      ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. In IEEE International Conference on Software Quality, Reliability and Security - QRS 2017. Neuveden: IEEE. s. 54-64. ISBN 978-1-5386-0592-9. doi:10.1109/QRS.2017.15. 2017.
      URL
      RIV/00216224:14330/17:00095127 Stať ve sborníku. Informatika. angličtina.
      Štill, Vladimír (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: C++; Exceptions; Verification; Testing; Model Checking; DIVINE
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 10. 2018 16:25.
      Podrobněji: https://is.muni.cz/publication/1394157/cs

    2016

    1. DIVINE: Explicit-State LTL Model Checker
      ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. DIVINE: Explicit-State LTL Model Checker. In M. Chechik and J.-F. Raskin. Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. New York, NY, USA: Springer-Verlag New York, Inc. s. 920-922. ISBN 978-3-662-49673-2. doi:10.1007/978-3-662-49674-9_60. 2016.
      URL
      RIV/00216224:14330/16:00088093 Stať ve sborníku. Informatika. angličtina. Německo.
      Štill, Vladimír (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: DIVINE model checker; LTL model checking
      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:25.
      Podrobněji: https://is.muni.cz/publication/1352234/cs
    2. On verifying C++ programs with probabilities
      BARNAT, Jiří, Ivana ČERNÁ, Petr ROČKAI, Vladimír ŠTILL a Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities. In Sascha Ossowski. Proceedings of the 31st Annual ACM Symposium on Applied Computing. Pisa: ACM New York, NY, USA. s. 1238-1243. ISBN 978-1-4503-3739-7. doi:10.1145/2851613.2851721. 2016.
      URL
      Název anglicky: On verifying {C++} programs with probabilities
      RIV/00216224:14330/16:00088057 Stať ve sborníku. Informatika. angličtina. Itálie.
      Barnat, Jiří (203 Česká republika, garant, domácí) -- Černá, Ivana (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Zákopčanová, Kristína (203 Česká republika, domácí)
      Klíčová slova anglicky: Model Checking; Probabilistic systems; DIVINE ; PRISM
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 16. 7. 2018 15:46.
      Podrobněji: https://is.muni.cz/publication/1350754/cs
    3. Weak Memory Models as LLVM-to-LLVM Transformations
      ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. In Jan Kofroň and Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop. Neuveden: Springer. s. 144-155. ISBN 978-3-319-29816-0. doi:10.1007/978-3-319-29817-7_13. 2016.
      URL
      RIV/00216224:14330/16:00088094 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Štill, Vladimír (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: memory models; 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: 13. 5. 2020 19:15.
      Podrobněji: https://is.muni.cz/publication/1352236/cs

    2015

    1. Fast, Dynamically-Sized Concurrent Hash Table
      BARNAT, Jiří, Petr ROČKAI, Vladimír ŠTILL a Jiří WEISER. Fast, Dynamically-Sized Concurrent Hash Table. In Bernd Fischer, Jaco Geldenhuys. Model Checking Software. Neuveden: Springer International Publishing. s. 49-65. ISBN 978-3-319-23403-8. doi:10.1007/978-3-319-23404-5_5. 2015.
      RIV/00216224:14330/15:00081182 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Barnat, Jiří (203 Česká republika, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, garant, domácí) -- Weiser, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: Data Structures; Concurrency; Hash Tables; Model Checking; DIVINE; C++
      Druh sborníku: postkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 16. 11. 2015 10:32.
      Podrobněji: https://is.muni.cz/publication/1316723/cs
    2. Techniques for Memory-Efficient Model Checking of C and C++ Code
      ROČKAI, Petr, Vladimír ŠTILL a Jiří BARNAT. Techniques for Memory-Efficient Model Checking of C and C++ Code. In Radu Calinescu, Bernhard Rumpe. Software Engineering and Formal Methods. Neuveden: Springer International Publishing. s. 268-282. ISBN 978-3-319-22968-3. doi:10.1007/978-3-319-22969-0_19. 2015.
      RIV/00216224:14330/15:00081181 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, garant, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: LLVM; model checking; compression; memory-efficient; explicit-state
      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:49.
      Podrobněji: https://is.muni.cz/publication/1316721/cs

    2014

    1. Context-Switch-Directed Verification in DIVINE
      ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Context-Switch-Directed Verification in DIVINE. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. Mathematical and Engineering Methods in Computer Science. Neuveden: Springer International Publishing. s. 135-146. ISBN 978-3-319-14895-3. doi:10.1007/978-3-319-14896-0_12. 2014.
      RIV/00216224:14330/14:00084599 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Štill, Vladimír (203 Česká republika, garant, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: model checking; LLVM; context-switch bounded verification
      Druh sborníku: předkonferenční sborník
      Mezinárodní význam: ano
      Recenzováno: ano
      Změnil: RNDr. Vladimír Štill, Ph.D., učo 373979. Změněno: 9. 11. 2015 12:23.
      Podrobněji: https://is.muni.cz/publication/1316718/cs

    2013

    1. DIVINE 3.0 (software)
      ROČKAI, Petr, Jiří BARNAT, Vladimír ŠTILL, Jiří WEISER, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK a Jan KRIHO. DIVINE 3.0. 2013.
      zdrojový kód URL
      RIV/00216224:14330/13:00072941 Software. Informatika. angličtina. Česká republika.
      Ročkai, Petr (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Weiser, Jiří (203 Česká republika, domácí) -- Brim, Luboš (203 Česká republika, domácí) -- Havel, Vojtěch (203 Česká republika, domácí) -- Havlíček, Jan (203 Česká republika, domácí) -- Kriho, Jan (203 Česká republika, domácí)
      Klíčová slova anglicky: distributed-memory computing; LTL model checking; Partial Order Reduction; On-The-Fly verification; LLVM; Software Model Checking
      Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 23. 4. 2014 12:49.
      Podrobněji: https://is.muni.cz/publication/1179466/cs
    2. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
      BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO, Milan LENČO, Petr ROČKAI, Vladimír ŠTILL a Jiří WEISER. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Sharygina, Natasha; Veith, Helmut. Computer Aided Verification 2013. Heidelberg: Springer. s. 863-868. ISBN 978-3-642-39798-1. doi:10.1007/978-3-642-39799-8_60. 2013.
      Název česky: DiVinE 3.0 -- Explicitně-stavový nástroj pro ověřování modelu pro vícevláknové C a C++ programy
      RIV/00216224:14330/13:00066526 Stať ve sborníku. Informatika. angličtina. Německo.
      Barnat, Jiří (203 Česká republika, garant, domácí) -- Brim, Luboš (203 Česká republika, domácí) -- Havel, Vojtěch (203 Česká republika, domácí) -- Havlíček, Jan (203 Česká republika, domácí) -- Kriho, Jan (203 Česká republika, domácí) -- Lenčo, Milan (703 Slovensko, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Štill, Vladimír (203 Česká republika, domácí) -- Weiser, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: model checking; LLVM; C++; C; LTL; timed automata
      Druh sborníku: předkonferenční sborník
      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2014 23:39.
      Podrobněji: https://is.muni.cz/publication/1130026/cs
Zobrazeno: 20. 4. 2024 07:34