Masaryk University

Publication Records

česky | in English

Filter publications

    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Á and Tadeáš KUČERA. DIVINE 4.4. 2021.
      URL zdrojový kód
      RIV/00216224:14330/21:00119996 Software. English. Czech Republic.
      Ročkai, Petr (703 Slovakia, guarantor, belonging to the institution) -- Lauko, Henrich (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Baranová, Zuzana (703 Slovakia) -- Korenčik, Lukáš (703 Slovakia) -- Matoušek, Adam (203 Czech Republic) -- Barnat, Jiří (203 Czech Republic) -- Šárník, Jakub (203 Czech Republic) -- Mrázek, Jan (203 Czech Republic) -- Kejstová, Katarína (703 Slovakia) -- Kučera, Tadeáš (203 Czech Republic)
      Keywords in English: model checking; correctness; analysis; concurrency; symbolic
      International impact: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 6/11/2023 10:42.
      More: https://is.muni.cz/publication/1836137/en

    2019

    1. Extending DIVINE with Symbolic Verification Using SMT
      LAUKO, Henrich, Vladimír ŠTILL, Petr ROČKAI and 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, 2019, p. 204-208. ISBN 978-3-030-17501-6. Available from: https://dx.doi.org/10.1007/978-3-030-17502-3_14.
      URL
      RIV/00216224:14330/19:00107528 Proceedings paper. English. Switzerland.
      Lauko, Henrich (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 07:37.
      More: https://is.muni.cz/publication/1547580/en
    2. Local Nontermination Detection for Parallel C++ Programs
      ŠTILL, Vladimír and 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, 2019, p. 373-390. ISBN 978-3-030-30445-4. Available from: https://dx.doi.org/10.1007/978-3-030-30446-1_20.
      Author's page Publisher's page
      RIV/00216224:14330/19:00107759 Proceedings paper. English. Switzerland.
      Štill, Vladimír (203 Czech Republic, guarantor, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: termination; nontermination; local nontermination; parallel programs; c++; model checking; DIVINE
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2020 00:04.
      More: https://is.muni.cz/publication/1576677/en

    2018

    1. DiVM: Model checking with LLVM and graph memory
      ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ and Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. Journal of Systems and Software. Elsevier, 2018, vol. 143, Oct, p. 1-13. ISSN 0164-1212. Available from: https://dx.doi.org/10.1016/j.jss.2018.04.026.
      URL
      RIV/00216224:14330/18:00106878 Article in a journal. English. Netherlands.
      Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Černá, Ivana (203 Czech Republic, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: Model checking; C plus; Virtual machine; Verification
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 5/11/2021 15:28.
      More: https://is.muni.cz/publication/1528139/en
    2. Model Checking of C++ Programs Under the x86-TSO Memory Model
      ŠTILL, Vladimír and 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, 2018, p. 124-140. ISBN 978-3-030-02449-9. Available from: https://dx.doi.org/10.1007/978-3-030-02450-5_8.
      Publisher's page Author's page
      RIV/00216224:14330/18:00101450 Proceedings paper. English. Switzerland.
      Štill, Vladimír (203 Czech Republic, guarantor, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: relaxed memory; model checking; c++; x86; memory model; DIVINE
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 30/4/2019 07:36.
      More: https://is.muni.cz/publication/1479960/en

    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 and 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, 2017, p. 201-207. ISBN 978-3-319-68166-5. Available from: https://dx.doi.org/10.1007/978-3-319-68167-2_14.
      URL
      RIV/00216224:14330/17:00095126 Proceedings paper. Informatics. English. Switzerland.
      Baranová, Zuzana (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Kejstová, Katarína (703 Slovakia, belonging to the institution) -- Kučera, Tadeáš (203 Czech Republic, belonging to the institution) -- Lauko, Henrich (703 Slovakia, belonging to the institution) -- Mrázek, Jan (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution)
      Keywords in English: Model Checking; Verification; C; C++; DIVINE
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/10/2018 16:24.
      More: https://is.muni.cz/publication/1394153/en
    2. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
      MRÁZEK, Jan, Martin JONÁŠ, Vladimír ŠTILL, Henrich LAUKO and 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, 2017, p. 390-393. ISBN 978-3-662-54579-9. Available from: https://dx.doi.org/10.1007/978-3-662-54580-5_29.
      URL
      RIV/00216224:14330/17:00095131 Proceedings paper. Informatics. English. Germany.
      Mrázek, Jan (203 Czech Republic, belonging to the institution) -- Jonáš, Martin (203 Czech Republic, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Lauko, Henrich (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: program verification; model checking; formula optimizations; caching
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:23.
      More: https://is.muni.cz/publication/1394228/en
    3. Using Off-the-Shelf Exception Support Components in C++ Verification
      ŠTILL, Vladimír, Petr ROČKAI and Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. Online. In IEEE International Conference on Software Quality, Reliability and Security - QRS 2017. Neuveden: IEEE, 2017, p. 54-64. ISBN 978-1-5386-0592-9. Available from: https://dx.doi.org/10.1109/QRS.2017.15.
      URL
      RIV/00216224:14330/17:00095127 Proceedings paper. Informatics. English.
      Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: C++; Exceptions; Verification; Testing; Model Checking; DIVINE
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/10/2018 16:25.
      More: https://is.muni.cz/publication/1394157/en

    2016

    1. DIVINE: Explicit-State LTL Model Checker
      ŠTILL, Vladimír, Petr ROČKAI and 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., 2016, p. 920-922. ISBN 978-3-662-49673-2. Available from: https://dx.doi.org/10.1007/978-3-662-49674-9_60.
      URL
      RIV/00216224:14330/16:00088093 Proceedings paper. Informatics. English. Germany.
      Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: DIVINE model checker; LTL model checking
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:25.
      More: https://is.muni.cz/publication/1352234/en
    2. On verifying C++ programs with probabilities (On verifying {C++} programs with probabilities)
      BARNAT, Jiří, Ivana ČERNÁ, Petr ROČKAI, Vladimír ŠTILL and Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities (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, 2016, p. 1238-1243. ISBN 978-1-4503-3739-7. Available from: https://dx.doi.org/10.1145/2851613.2851721.
      URL
      Name (in English): On verifying {C++} programs with probabilities
      RIV/00216224:14330/16:00088057 Proceedings paper. Informatics. English. Italy.
      Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Černá, Ivana (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Zákopčanová, Kristína (203 Czech Republic, belonging to the institution)
      Keywords in English: Model Checking; Probabilistic systems; DIVINE ; PRISM
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 16/7/2018 15:46.
      More: https://is.muni.cz/publication/1350754/en
    3. Weak Memory Models as LLVM-to-LLVM Transformations
      ŠTILL, Vladimír, Petr ROČKAI and Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. Online. In Jan Kofroň and Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop. Neuveden: Springer, 2016, p. 144-155. ISBN 978-3-319-29816-0. Available from: https://dx.doi.org/10.1007/978-3-319-29817-7_13.
      URL
      RIV/00216224:14330/16:00088094 Proceedings paper. Informatics. English. Switzerland.
      Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
      Keywords in English: memory models; model checking
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:15.
      More: https://is.muni.cz/publication/1352236/en

    2015

    1. Fast, Dynamically-Sized Concurrent Hash Table
      BARNAT, Jiří, Petr ROČKAI, Vladimír ŠTILL and Jiří WEISER. Fast, Dynamically-Sized Concurrent Hash Table. In Bernd Fischer, Jaco Geldenhuys. Model Checking Software. Neuveden: Springer International Publishing, 2015, p. 49-65. ISBN 978-3-319-23403-8. Available from: https://dx.doi.org/10.1007/978-3-319-23404-5_5.
      RIV/00216224:14330/15:00081182 Proceedings paper. Informatics. English. Switzerland.
      Barnat, Jiří (203 Czech Republic, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, guarantor, belonging to the institution) -- Weiser, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: Data Structures; Concurrency; Hash Tables; Model Checking; DIVINE; C++
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 16/11/2015 10:32.
      More: https://is.muni.cz/publication/1316723/en
    2. Techniques for Memory-Efficient Model Checking of C and C++ Code
      ROČKAI, Petr, Vladimír ŠTILL and 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, 2015, p. 268-282. ISBN 978-3-319-22968-3. Available from: https://dx.doi.org/10.1007/978-3-319-22969-0_19.
      RIV/00216224:14330/15:00081181 Proceedings paper. Informatics. English. Switzerland.
      Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, guarantor, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: LLVM; model checking; compression; memory-efficient; explicit-state
      Type of proceedings: post-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 20:49.
      More: https://is.muni.cz/publication/1316721/en

    2014

    1. Context-Switch-Directed Verification in DIVINE
      ŠTILL, Vladimír, Petr ROČKAI and 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, 2014, p. 135-146. ISBN 978-3-319-14895-3. Available from: https://dx.doi.org/10.1007/978-3-319-14896-0_12.
      RIV/00216224:14330/14:00084599 Proceedings paper. Informatics. English. Switzerland.
      Štill, Vladimír (203 Czech Republic, guarantor, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: model checking; LLVM; context-switch bounded verification
      Type of proceedings: pre-proceedings
      International impact: yes
      Reviewed: yes
      Changed by: RNDr. Vladimír Štill, Ph.D., učo 373979. Changed: 9/11/2015 12:23.
      More: https://is.muni.cz/publication/1316718/en

    2013

    1. DIVINE 3.0 (software)
      ROČKAI, Petr, Jiří BARNAT, Vladimír ŠTILL, Jiří WEISER, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK and Jan KRIHO. DIVINE 3.0. 2013.
      zdrojový kód URL
      RIV/00216224:14330/13:00072941 Software. Informatics. English. Czech Republic.
      Ročkai, Petr (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Weiser, Jiří (203 Czech Republic, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution) -- Havel, Vojtěch (203 Czech Republic, belonging to the institution) -- Havlíček, Jan (203 Czech Republic, belonging to the institution) -- Kriho, Jan (203 Czech Republic, belonging to the institution)
      Keywords in English: distributed-memory computing; LTL model checking; Partial Order Reduction; On-The-Fly verification; LLVM; Software Model Checking
      Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 23/4/2014 12:49.
      More: https://is.muni.cz/publication/1179466/en
    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 and 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, 2013, p. 863-868. ISBN 978-3-642-39798-1. Available from: https://dx.doi.org/10.1007/978-3-642-39799-8_60.
      Name in Czech: 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 Proceedings paper. Informatics. English. Germany.
      Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution) -- Brim, Luboš (203 Czech Republic, belonging to the institution) -- Havel, Vojtěch (203 Czech Republic, belonging to the institution) -- Havlíček, Jan (203 Czech Republic, belonging to the institution) -- Kriho, Jan (203 Czech Republic, belonging to the institution) -- Lenčo, Milan (703 Slovakia, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Štill, Vladimír (203 Czech Republic, belonging to the institution) -- Weiser, Jiří (203 Czech Republic, belonging to the institution)
      Keywords in English: model checking; LLVM; C++; C; LTL; timed automata
      Type of proceedings: pre-proceedings
      Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 27/4/2014 23:39.
      More: https://is.muni.cz/publication/1130026/en
Displayed: 3/5/2024 10:50