Masaryk University

Publication Records

česky | in English

Filter publications

    2020

  1. LAUKO, Henrich, Martina OLLIARO, Agostino CORTESI and Petr ROČKAI. Abstracting Strings for Model Checking of C Programs. Applied Sciences. Multidisciplinary Digital Publishing Institute, 2020, vol. 10, No 21, p. 1-33. ISSN 2076-3417. doi:10.3390/app10217853.
    URL
    RIV/00216224:14330/20:00114537 Article in a journal. English. Switzerland.
    Lauko, Henrich (703 Slovakia, belonging to the institution) -- Olliaro, Martina (380 Italy, belonging to the institution) -- Cortesi, Agostino (380 Italy) -- Ročkai, Petr (203 Czech Republic, belonging to the institution)
    Keywords in English: string analysis; model checking; abstract interpretation; abstract domain
    International impact: yes
    Reviewed: yes

    Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2021 08:11.
  2. KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO and Jiří BARNAT. On Symbolic Execution of Decompiled Programs. In Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020. Neuveden: IEEE Computer Society, 2020. p. 265-272. ISBN 978-1-7281-8914-7. doi:10.1109/QRS51102.2020.00044.
    RIV/00216224:14330/20:00114781 Proceedings paper. English. United States of America.
    Korenčik, Lukáš (703 Slovakia, belonging to the institution) -- Ročkai, Petr (703 Slovakia, belonging to the institution) -- Lauko, Henrich (703 Slovakia, belonging to the institution) -- Barnat, Jiří (203 Czech Republic, belonging to the institution)
    Keywords in English: symbolic execution; decompilation; model checking; llvm
    International impact: yes
    Reviewed: yes

    Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2021 08:16.
  3. 2019

  4. 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. doi: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.
  5. ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO and Agostino CORTESI. String Abstraction for Model Checking of C Programs. In Fabrizio Biondi, Thomas Given-Wilson, Axel Legay. Model Checking Software. Cham: Springer International Publishing, 2019. p. 74-93. ISBN 978-3-030-30922-0. doi:10.1007/978-3-030-30923-7_5.
    URL
    RIV/00216224:14330/19:00107758 Proceedings paper. English. Switzerland.
    Ročkai, Petr (703 Slovakia, belonging to the institution) -- Lauko, Henrich (703 Slovakia, guarantor, belonging to the institution) -- Olliaro, Martina (380 Italy, belonging to the institution) -- Cortesi, Agostino (380 Italy)
    Keywords in English: Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
    International impact: yes

    Changed by: Martina Olliaro, Ph.D., učo 477767. Changed: 11/9/2020 09:45.
  6. 2018

  7. LAUKO, Henrich, Petr ROČKAI and Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018. p. 313-332. ISBN 978-3-030-02507-6. doi:10.1007/978-3-030-02508-3_17.
    URL
    RIV/00216224:14330/18:00101301 Proceedings paper. English. Switzerland.
    Lauko, Henrich (703 Slovakia) -- Ročkai, Petr (703 Slovakia) -- Barnat, Jiří (203 Czech Republic, guarantor, belonging to the institution)
    Keywords in English: Symbolic Computation; Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
    Type of proceedings: post-proceedings
    International impact: yes
    Reviewed: yes

    Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 30/4/2019 07:35.
  8. 2017

  9. 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. doi: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.
  10. 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. doi: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.
  11. 2016

  12. MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO and Jiří BARNAT. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Dragan Bošnački and Anton Wijs. Model Checking Software. Neuveden: Springer International Publishing, 2016. p. 208-213. ISBN 978-3-319-32581-1. doi:10.1007/978-3-319-32582-8_14.
    RIV/00216224:14330/16:00088095 Proceedings paper. Informatics. English. Switzerland.
    Mrázek, Jan (203 Czech Republic, belonging to the institution) -- Bauch, Petr (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: Model checking; C++; Symbolic approach
    Type of proceedings: pre-proceedings
    International impact: yes
    Reviewed: yes

    Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 27/4/2017 06:45.
Displayed: 19/1/2022 15:44