Masarykova univerzita

Výpis publikací

česky | in English

Filtrování publikací

    2022

  1. DivSIM , an interactive simulator for LLVM bitcode
    ROČKAI, Petr a Jiří BARNAT. DivSIM , an interactive simulator for LLVM bitcode. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. GERMANY: SPRINGER HEIDELBERG, 2022, roč. 24, č. 3, s. 493-510. ISSN 1433-2779. doi:10.1007/s10009-022-00659-x.
    Podrobněji: https://is.muni.cz/publication/1875255/cs
  2. LART: Compiled Abstract Execution (Competition Contribution)
    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, 2022. s. 457-461. ISBN 978-3-030-99526-3. doi:10.1007/978-3-030-99527-0_31.
    Podrobněji: https://is.muni.cz/publication/1828538/cs
  3. Verification of Programs Sensitive to Heap Layout
    LAUKO, 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. doi:10.1145/3508363.
    Podrobněji: https://is.muni.cz/publication/1828537/cs

    4. 2021

  4. 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.
    Podrobněji: https://is.muni.cz/publication/1836137/cs
  5. Reproducible execution of POSIX programs with DiOS
    ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. Software & Systems Modeling. Springer, 2021, roč. 20, č. 2, s. 363-382. ISSN 1619-1366. doi:10.1007/s10270-020-00837-y.
    Podrobněji: https://is.muni.cz/publication/1688018/cs

    6. 2020

  6. Abstracting Strings for Model Checking of C Programs
    LAUKO, 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. doi:10.3390/app10217853.
    Podrobněji: https://is.muni.cz/publication/1704118/cs
  7. Compiling C and C++ Programs for Dynamic White-Box Analysis
    BARANOVÁ, Zuzana a Petr ROČKAI. Compiling C and C++ Programs for Dynamic White-Box Analysis. In Nelma Moreira and Emil Sekerinski. Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). Cham: Springer International Publishing, 2020. s. 30-45. ISBN 978-3-030-54993-0. doi:10.1007/978-3-030-54994-7_4.
    Podrobněji: https://is.muni.cz/publication/1592136/cs
  8. Model checking in a development workflow: A study on a concurrent C++ hash table
    ROČKAI, Petr. Model checking in a development workflow: A study on a concurrent C++ hash table. In Nelma Moreira and Emil Sekerinski. Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). Cham: Springer International Publishing, 2020. s. 46-60. ISBN 978-3-030-54993-0. doi:10.1007/978-3-030-54994-7_5.
    Podrobněji: https://is.muni.cz/publication/1688016/cs
  9. On Symbolic Execution of Decompiled Programs
    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, 2020. s. 265-272. ISBN 978-1-7281-8914-7. doi:10.1109/QRS51102.2020.00044.
    Podrobněji: https://is.muni.cz/publication/1760802/cs

    10. 2019

  10. A Simulator for LLVM Bitcode
    ROČKAI, Petr a Jiří BARNAT. A Simulator for LLVM Bitcode. In K. G. Larsen, T. Willemse. 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019. Scham: Springer Verlag, 2019. s. 127-142. ISBN 978-3-030-27007-0. doi:10.1007/978-3-030-27008-7_8.
    Podrobněji: https://is.muni.cz/publication/1577797/cs
  11. 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, 2019. s. 204-208. ISBN 978-3-030-17501-6. doi:10.1007/978-3-030-17502-3_14.
    Podrobněji: https://is.muni.cz/publication/1547580/cs
  12. Reproducible Execution of POSIX Programs with DiOS
    ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible Execution of POSIX Programs with DiOS. In Peter Csaba Ölveczky and Gwen Salaün. Software Engineering and Formal Methods. 17th ed. Cham: Springer International Publishing, 2019. s. 333-349. ISBN 978-3-030-30445-4. doi:10.1007/978-3-030-30446-1_18.
    Podrobněji: https://is.muni.cz/publication/1577576/cs
  13. String Abstraction for Model Checking of C Programs
    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, 2019. s. 74-93. ISBN 978-3-030-30922-0. doi:10.1007/978-3-030-30923-7_5.
    Podrobněji: https://is.muni.cz/publication/1576598/cs

    14. 2018

  14. 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, 2018, roč. 143, Oct, s. 1-13. ISSN 0164-1212. doi:10.1016/j.jss.2018.04.026.
    Podrobněji: https://is.muni.cz/publication/1528139/cs
  15. Symbolic Computation via Program Transformation
    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, 2018. s. 313-332. ISBN 978-3-030-02507-6. doi:10.1007/978-3-030-02508-3_17.
    Podrobněji: https://is.muni.cz/publication/1459216/cs

    16. 2017

  16. From Model Checking to Runtime Verification and Back
    KEJSTOVÁ, Katarína, Petr ROČKAI a Jiří BARNAT. From Model Checking to Runtime Verification and Back. In Shuvendu Lahiri, Giles Reger. Runtime Verification - 17th International Conference, RV 2017. neuvedeno: Springer, 2017. s. 225-240. ISBN 978-3-319-67530-5. doi:10.1007/978-3-319-67531-2_14.
    Podrobněji: https://is.muni.cz/publication/1394289/cs
  17. 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, 2017. s. 201-207. ISBN 978-3-319-68166-5. doi:10.1007/978-3-319-68167-2_14.
    Podrobněji: https://is.muni.cz/publication/1394153/cs
  18. 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, 2017. s. 54-64. ISBN 978-1-5386-0592-9. doi:10.1109/QRS.2017.15.
    Podrobněji: https://is.muni.cz/publication/1394157/cs

    19. 2016

  19. 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., 2016. s. 920-922. ISBN 978-3-662-49673-2. doi:10.1007/978-3-662-49674-9_60.
    Podrobněji: https://is.muni.cz/publication/1352234/cs
  20. Model checking C++ programs with exceptions
    ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, roč. 128, 15 October 2016, s. 68-85. ISSN 0167-6423. doi:10.1016/j.scico.2016.05.007.
    Podrobněji: https://is.muni.cz/publication/1352228/cs
  21. 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, 2016. s. 1238-1243. ISBN 978-1-4503-3739-7. doi:10.1145/2851613.2851721.
    Podrobněji: https://is.muni.cz/publication/1350754/cs
  22. 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, 2016. s. 144-155. ISBN 978-3-319-29816-0. doi:10.1007/978-3-319-29817-7_13.
    Podrobněji: https://is.muni.cz/publication/1352236/cs

    23. 2015

  23. 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, 2015. s. 49-65. ISBN 978-3-319-23403-8. doi:10.1007/978-3-319-23404-5_5.
    Podrobněji: https://is.muni.cz/publication/1316723/cs
  24. 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, 2015. s. 268-282. ISBN 978-3-319-22968-3. doi:10.1007/978-3-319-22969-0_19.
    Podrobněji: https://is.muni.cz/publication/1316721/cs

    25. 2014

  25. 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, 2014. s. 135-146. ISBN 978-3-319-14895-3. doi:10.1007/978-3-319-14896-0_12.
    Podrobněji: https://is.muni.cz/publication/1316718/cs
  26. Model Checking C++ with Exceptions
    ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Model Checking C++ with Exceptions. Electronic Communications of the EASST. 2014, roč. 70, Listopad, s. 1-15. ISSN 1863-2122. doi:10.14279/tuj.eceasst.70.983.
    Podrobněji: https://is.muni.cz/publication/1210603/cs

    27. 2013

  27. Distributed LTL Model Checking with Hash Compaction
    BARNAT, Jiří, Jan HAVLÍČEK a Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013. s. 79-93. ISSN 1571-0661. doi:10.1016/j.entcs.2013.07.006.
    Podrobněji: https://is.muni.cz/publication/1082157/cs
  28. 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.
    Podrobněji: https://is.muni.cz/publication/1179466/cs
  29. 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, 2013. s. 863-868. ISBN 978-3-642-39798-1. doi:10.1007/978-3-642-39799-8_60.
    Podrobněji: https://is.muni.cz/publication/1130026/cs
  30. Improved State Space Reductions for LTL Model Checking of C & C++ Programs
    ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. In Guillaume Brat, Neha Rungta, Arnaud Venet. NASA Formal Methods 2013. Neuveden: Springer, 2013. s. 1-15. ISBN 978-3-642-38087-7. doi:10.1007/978-3-642-38088-4_1.
    Podrobněji: https://is.muni.cz/publication/1130020/cs

    31. 2012

  31. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming. Elsevier, 2012, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. doi:10.1016/j.scico.2011.03.001.
    Podrobněji: https://is.muni.cz/publication/955939/cs
  32. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs
    BARNAT, Jiří, Jan BERAN, Luboš BRIM, Tomáš KRATOCHVÍLA a Petr ROČKAI. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical Systems (FMICS 2012). Berlin: Springer Berlin Heidelberg, 2012. s. 78--92. ISBN 978-3-642-32468-0. doi:10.1007/978-3-642-32469-7_6.
    Podrobněji: https://is.muni.cz/publication/1075277/cs
  33. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg, 2012. s. 252-266. ISBN 978-3-642-28890-6. doi:10.1007/978-3-642-28891-3_25.
    Podrobněji: https://is.muni.cz/publication/979265/cs

    34. 2010

  34. DiVinE: Parallel Distributed Model Checker (Tool paper)
    BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA a Petr ROČKAI. DiVinE: Parallel Distributed Model Checker (Tool paper). In Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010). 2010. 4 s.
    Podrobněji: https://is.muni.cz/publication/905387/cs
  35. DiVinE 2.4 (software)
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE 2.4. 2010.
    Podrobněji: https://is.muni.cz/publication/935957/cs
  36. Parallel Partial Order Reduction with Topological Sort Proviso
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010. s. 222-231. ISBN 978-0-7695-4153-2.
    Podrobněji: https://is.muni.cz/publication/913444/cs
  37. Scalable shared memory LTL model checking
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, roč. 12, č. 2, s. 139-153. ISSN 1433-2779. doi:10.1007/s10009-010-0136-z.
    Podrobněji: https://is.muni.cz/publication/886012/cs

    38. 2009

  38. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany: Springer Berlin / Heidelberg, 2009. s. 407-425. ISBN 978-3-642-10372-8. doi:10.1007/978-3-642-10373-5_21.
    Podrobněji: https://is.muni.cz/publication/860162/cs
  39. DiVinE 2.0 (software)
    ROČKAI, Petr, Jiří BARNAT, Luboš BRIM a Milan ČEŠKA. DiVinE 2.0. 2009.
    Podrobněji: https://is.muni.cz/publication/875229/cs
  40. DiVinE 2.0: High-Performance Model Checking
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE 2.0: High-Performance Model Checking. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009. s. 31-32. ISBN 978-0-7695-3809-9.
    Podrobněji: https://is.muni.cz/publication/856390/cs

    41. 2008

  41. DiVinE Multi-Core -- A Parallel LTL Model-Checker
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008. s. 234-239. ISBN 978-3-540-88386-9.
    Podrobněji: https://is.muni.cz/publication/792976/cs
  42. Shared Hash Tables in Parallel Model Checking
    BARNAT, Jiří a Petr ROČKAI. Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science. Elsevier, 2008, roč. 2008, 198(1), s. 79-91, 12 s. ISSN 1571-0661.
    Podrobněji: https://is.muni.cz/publication/760855/cs

    43. 2007

  43. DiVinE Multi-Core (software)
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core. 2007.
    Podrobněji: https://is.muni.cz/publication/759931/cs
  44. Scalable Multi-core LTL Model-Checking
    BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1. vyd. Berlin, Heidelberg: Springer-Verlag, 2007. s. 187-203. ISBN 978-3-540-73369-0.
    Podrobněji: https://is.muni.cz/publication/720747/cs

    45. 2006

  45. DiVinE -- A Tool for Distributed Verification
    BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Pavel MORAVEC, Petr ROČKAI a Pavel ŠIMEČEK. DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin: Springer Verlag, 2006. s. 278-281. ISBN 978-3-540-37406-0.
    Podrobněji: https://is.muni.cz/publication/702305/cs
Zobrazit podrobně
Zobrazeno: 2. 10. 2023 14:15