Masarykova univerzita

Výpis publikací

česky | in English

Filtrování publikací

    2022

    1. DURET-LUTZ, Alexandre, Etienne RENAULT, Maximilien COLANGE, Florian RENKIN, Alexandre Gbaguidi AISSE, Philipp SCHLEHUBER-CAISSIER, Thomas MEDIONI, Antoine MARTIN, Jérôme DUBOIS, Clément GILLARD a Henrich LAUKO. From Spot 2.0 to Spot 2.10: What's New? In Sharon Shoham, Yakir Vizel. Computer Aided Verification. Cham: Springer International Publishing. s. 174-187, 13 s. ISBN 978-3-031-13188-2. doi:10.1007/978-3-031-13188-2_9. 2022.
      angličtina. Švýcarsko.
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Henrich Lauko, učo 410438. Změněno: 24. 7. 2023 11:04.
    2. LART (software)
      LAUKO, Henrich. LART. 2022.
      URL
      angličtina. Česká republika.
      Klíčová slova anglicky: compiler;program instrumentation;abstraction;llvm

      Změnil: RNDr. Henrich Lauko, učo 410438. Změněno: 10. 11. 2023 11:02.
    3. LAUKO, Henrich a Petr ROČKAI. LART: Compiled Abstract Execution (Competition Contribution). In Fisman, Dana and Rosu, Grigore. TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing. s. 457-461. ISBN 978-3-030-99526-3. doi:10.1007/978-3-030-99527-0_31. 2022.
      RIV/00216224:14330/22:00125302 Stať ve sborníku. angličtina.
      Lauko, Henrich (703 Slovensko, domácí) -- Ročkai, Petr (703 Slovensko, garant, domácí)
      Klíčová slova anglicky: abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 6. 4. 2023 08:35.
    4. LAUKO, Henrich, Lukáš KORENČIK a Petr ROČKAI. Verification of Programs Sensitive to Heap Layout. ACM Transactions on Software Engineering and Methodology. roč. 31, č. 4, s. 1-27. ISSN 1049-331X. doi:10.1145/3508363. 2022.
      domovská stránka výsledku URL
      RIV/00216224:14330/22:00125301 Článek v odborném periodiku. angličtina. Spojené státy.
      Lauko, Henrich (703 Slovensko, domácí) -- Korenčik, Lukáš (703 Slovensko, domácí) -- Ročkai, Petr (703 Slovensko, garant, domácí)
      Klíčová slova anglicky: heap;pointers;abstraction;refinement;program transformation
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 6. 4. 2023 08:20.

    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.

    2020

    1. LAUKO, Henrich, Martina OLLIARO, Agostino CORTESI a Petr ROČKAI. Abstracting Strings for Model Checking of C Programs. Applied Sciences. Multidisciplinary Digital Publishing Institute, roč. 10, č. 21, s. 1-33. ISSN 2076-3417. doi:10.3390/app10217853. 2020.
      URL
      RIV/00216224:14330/20:00114537 Článek v odborném periodiku. angličtina. Švýcarsko.
      Lauko, Henrich (703 Slovensko, domácí) -- Olliaro, Martina (380 Itálie, domácí) -- Cortesi, Agostino (380 Itálie) -- Ročkai, Petr (203 Česká republika, domácí)
      Klíčová slova anglicky: string analysis; model checking; abstract interpretation; abstract domain
      Mezinárodní význam: ano
      Recenzováno: ano

      Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 08:11.
    2. KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO a 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. s. 265-272. ISBN 978-1-7281-8914-7. doi:10.1109/QRS51102.2020.00044. 2020.
      RIV/00216224:14330/20:00114781 Stať ve sborníku. angličtina. Spojené státy.
      Korenčik, Lukáš (703 Slovensko, domácí) -- Ročkai, Petr (703 Slovensko, domácí) -- Lauko, Henrich (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, domácí)
      Klíčová slova anglicky: symbolic execution; decompilation; model checking; llvm
      Mezinárodní význam: ano
      Recenzováno: ano

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

    2019

    1. 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.
    2. ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO a 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. s. 74-93. ISBN 978-3-030-30922-0. doi:10.1007/978-3-030-30923-7_5. 2019.
      URL
      RIV/00216224:14330/19:00107758 Stať ve sborníku. angličtina. Švýcarsko.
      Ročkai, Petr (703 Slovensko, domácí) -- Lauko, Henrich (703 Slovensko, garant, domácí) -- Olliaro, Martina (380 Itálie, domácí) -- Cortesi, Agostino (380 Itálie)
      Klíčová slova anglicky: Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
      Mezinárodní význam: ano

      Změnila: Martina Olliaro, Ph.D., učo 477767. Změněno: 11. 9. 2020 09:45.

    2018

    1. LAUKO, Henrich, Petr ROČKAI a Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer. s. 313-332. ISBN 978-3-030-02507-6. doi:10.1007/978-3-030-02508-3_17. 2018.
      URL
      RIV/00216224:14330/18:00101301 Stať ve sborníku. angličtina. Švýcarsko.
      Lauko, Henrich (703 Slovensko, 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++
      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: 20. 9. 2022 11:14.

    2017

    1. 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.
    2. 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.

    2016

    1. MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO a 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. s. 208-213. ISBN 978-3-319-32581-1. doi:10.1007/978-3-319-32582-8_14. 2016.
      RIV/00216224:14330/16:00088095 Stať ve sborníku. Informatika. angličtina. Švýcarsko.
      Mrázek, Jan (203 Česká republika, domácí) -- Bauch, Petr (203 Česká republika, domácí) -- Lauko, Henrich (703 Slovensko, domácí) -- Barnat, Jiří (203 Česká republika, garant, domácí)
      Klíčová slova anglicky: Model checking; C++; Symbolic approach
      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. 2017 06:45.
Zobrazeno: 29. 3. 2024 02:22