-
From Spot 2.0 to Spot 2.10: What's New? D - Stať ve sborníkuDURET-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?. Online. In Sharon Shoham, Yakir Vizel. Computer Aided Verification. Cham: Springer International Publishing, 2022, s. 174-187. ISBN 978-3-031-13187-5. Dostupné z: https://doi.org/10.1007/978-3-031-13188-2_9.Podrobněji: https://is.muni.cz/publication/2298917/cs
-
LART (software) R - SoftwareLAUKO, Henrich. LART. 2022.Podrobněji: https://is.muni.cz/publication/2335500/cs
-
LART: Compiled Abstract Execution (Competition Contribution) D - Stať ve sborníkuLAUKO, 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, 2022, s. 457-461. ISBN 978-3-030-99526-3. Dostupné z: https://doi.org/10.1007/978-3-030-99527-0_31.Podrobněji: https://is.muni.cz/publication/1828538/cs
-
Verification of Programs Sensitive to Heap Layout J - Článek v odborném periodikuLAUKO, Henrich; Lukáš KORENČIK a Petr ROČKAI. Verification of Programs Sensitive to Heap Layout. ACM Transactions on Software Engineering and Methodology. 2022, roč. 31, č. 4, s. 1-27. ISSN 1049-331X. Dostupné z: https://doi.org/10.1145/3508363.Podrobněji: https://is.muni.cz/publication/1828537/cs
-
DIVINE 4.4 (software) R - SoftwareROČ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.Podrobněji: https://is.muni.cz/publication/1836137/cs
-
Abstracting Strings for Model Checking of C Programs J - Článek v odborném periodikuLAUKO, Henrich; Martina OLLIARO; Agostino CORTESI a Petr ROČKAI. Abstracting Strings for Model Checking of C Programs. Applied Sciences. Multidisciplinary Digital Publishing Institute, 2020, roč. 10, č. 21, s. 1-33. ISSN 2076-3417. Dostupné z: https://doi.org/10.3390/app10217853.Podrobněji: https://is.muni.cz/publication/1704118/cs
-
On Symbolic Execution of Decompiled Programs D - Stať ve sborníkuKORENČ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, 2020, s. 265-272. ISBN 978-1-7281-8914-7. Dostupné z: https://doi.org/10.1109/QRS51102.2020.00044.Podrobněji: https://is.muni.cz/publication/1760802/cs
-
Extending DIVINE with Symbolic Verification Using SMT D - Stať ve sborníkuLAUKO, 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, 2019, s. 204-208. ISBN 978-3-030-17501-6. Dostupné z: https://doi.org/10.1007/978-3-030-17502-3_14.Podrobněji: https://is.muni.cz/publication/1547580/cs
-
String Abstraction for Model Checking of C Programs D - Stať ve sborníkuROČKAI, Petr; Henrich LAUKO; Martina OLLIARO a Agostino CORTESI. String Abstraction for Model Checking of C Programs. Online. In Fabrizio Biondi, Thomas Given-Wilson, Axel Legay. Model Checking Software. Cham: Springer International Publishing, 2019, s. 74-93. ISBN 978-3-030-30922-0. Dostupné z: https://doi.org/10.1007/978-3-030-30923-7_5.Podrobněji: https://is.muni.cz/publication/1576598/cs
-
Symbolic Computation via Program Transformation D - Stať ve sborníkuLAUKO, 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, 2018, s. 313-332. ISBN 978-3-030-02507-6. Dostupné z: https://doi.org/10.1007/978-3-030-02508-3_17.Podrobněji: https://is.muni.cz/publication/1459216/cs
-
Model Checking of C and C++ with DIVINE 4 D - Stať ve sborníkuBARANOVÁ, 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, 2017, s. 201-207. ISBN 978-3-319-68166-5. Dostupné z: https://doi.org/10.1007/978-3-319-68167-2_14.Podrobněji: https://is.muni.cz/publication/1394153/cs
-
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution) D - Stať ve sborníkuMRÁ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, 2017, s. 390-393. ISBN 978-3-662-54579-9. Dostupné z: https://doi.org/10.1007/978-3-662-54580-5_29.Podrobněji: https://is.muni.cz/publication/1394228/cs
-
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration D - Stať ve sborníkuMRÁ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, 2016, s. 208-213. ISBN 978-3-319-32581-1. Dostupné z: https://doi.org/10.1007/978-3-319-32582-8_14.Podrobněji: https://is.muni.cz/publication/1352238/cs