@misc{Rockai2008thesis,
    AUTHOR = "Petr Ročkai",
    TITLE = {Multi-Threaded Nested {DFS}},
    YEAR = "2008",
    TYPE = "Bachelor's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/139761/fi_b/",
    keywords = "divine"
}

@MastersThesis{Rockai2010thesis,
    AUTHOR = "Petr Ročkai",
    TITLE = {Partial Order Reduction in Parallel Model Checking},
    YEAR = "2010",
    TYPE = "Master's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/139761/fi_m/",
    keywords = "divine"
}

@Article{BBR10a,
  author =       "Jiří Barnat and Luboš Brim and Petr Ročkai",
  title =        {Scalable Shared Memory {LTL} Model Checking},
  journal =      "International Journal on Software Tools for Technology Transfer (STTT)",
  year =         "2010",
  volume =       "12",
  number =       "2",
  pages =        "139--153",
  url =          "http://dx.doi.org/10.1007/s10009-010-0136-z",
  optmonth =     "May",
  optnote =      "Special Section on SPIN 07"
}

@Article{BBS10,
  author =   "Jiří Barnat and Luboš Brim and David Šafránek",
  title =    {High-Performance Analysis of Biological Systems Dynamics with the {DiVinE} Model Checker},
  journal =  "Briefings in Bioinformatics",
  year =     "2010",
  volume =   "11",
  number =   "3",
  pages =    "301--312",
  url =      "http://dx.doi.org/10.1093/bib/bbp074",
  keywords = "divine"
}

@Article{BCP10,
  author =       "Jiří Barnat and Jakub Chaloupka and Jaco van de Pol",
  title =        {Distributed Algorithms for {SCC} Decomposition},
  journal =      "Journal of Logic and Computation",
  doi =          "10.1093/logcom/exp003",
  year =         "2010",
  url =          "http://logcom.oxfordjournals.org/cgi/content/abstract/exp003?ijkey=lCDPRRuADtjeFuo&keytype=ref",
  eprint =       "http://logcom.oxfordjournals.org/cgi/reprint/exp003v1.pdf",
  keywords = "divine"
}

@InProceedings{BBR10b,
  author =       "Jiří Barnat and Luboš Brim and Petr Ročkai",
  title =        {Parallel Partial Order Reduction with Topological Sort Proviso},
  booktitle =    {Proceeding of {SEFM} 2010},
  year =         "2010",
  publisher =    "IEEE Computer Society Press",
  keywords = "divine"

}

@InProceedings{barnat10parameter,
  author =       {Jiří Barnat and Luboš Brim and David Šafránek and Martin Vejnár},
  title =        {Parameter Scanning by Parallel Model Checking with
                  Applications in Systems Biology},
  booktitle =    {Proceedings of joint {HiBi/PDMC} workshop},
  year =         "2010",
  publisher =    "IEEE",
  keywords = "divine"
}

@InProceedings{barnat10employing,
  author =       {Jiří Barnat and Petr Bauch and Luboš Brim and Milan Češka},
  title =        {{Employing Multiple CUDA Devices to Accelerate LTL Model Checking}},
  booktitle =    {16th International Conference on Parallel and Distributed Systems ({ICPADS})},
  year =         "2010",
  publisher =    "IEEE",
  keywords = "divine"
}

@inproceedings{BBCR10DIVINE,
    title={{DiVinE}: Parallel Distributed Model Checker},
    author={Jiří Barnat and Luboš Brim and Milan Češka and Petr Ročkai},
    booktitle={Parallel and Distributed Methods in Verification and High
               Performance Computational Systems Biology},
    pages={4--7},
    year={2010},
    organization={IEEE},
    keywords={formal verification;parallel processing;reachability
        analysis;DiVinE;LTL model checking;parallel distributed model
            checker;reachability analysis, divine},
    doi={10.1109/PDMC-HiBi.2010.9},
    month={Sept}
}

@Inbook{BBR2012,
	author="Jiří Barnat and Luboš Brim and Petr Ročkai",
	editor="Goodloe, Alwyn E.
	and Person, Suzette",
	title="Towards LTL Model Checking of Unmodified Thread-Based C {\&} C++ Programs",
	bookTitle="NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings",
	year="2012",
	publisher="Springer Berlin Heidelberg",
	address="Berlin, Heidelberg",
	pages="252--266",
	isbn="978-3-642-28891-3",
	doi="10.1007/978-3-642-28891-3_25",
	url="http://dx.doi.org/10.1007/978-3-642-28891-3_25"
}

@article{BBR12OWCTY,
    title={On-the-fly Parallel Model Checking Algorithm that is Optimal for
           Verification of Weak {LTL} Properties},
    author={Jiří Barnat and Luboš Brim and Petr Ročkai},
    journal={Science of Computer Programming},
    volume={77},
    number={12},
    pages={1272--1288},
    month = oct,
    year={2012},
    issue_date = {October, 2012},
    issn = {0167-6423},
    numpages = {17},
    doi = {10.1016/j.scico.2011.03.001},
    acmid = {2350643},
    publisher = {Elsevier North-Holland, Inc.},
    address = {Amsterdam, The Netherlands, The Netherlands},
    keywords = {Explicit model checking, On-the-fly, Parallel, Partial order
        reduction, divine},
}

@misc{Havel2012thesis,
    AUTHOR = "Vojtěch Havel",
    TITLE = {Relaxed Memory Models in {DiVinE}},
    YEAR = "2012",
    TYPE = "Bachelor's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/359437/fi_b/",
    keywords = {divine}
}

@misc{Still2013thesis,
    AUTHOR = "Vladimír Štill",
    TITLE = {State Space Compression for the {DiVinE} Model Checker},
    YEAR = "2013",
    TYPE = "Bachelor's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/373979/fi_b/",
    keywords = {divine}
}

@misc{Weiser2013thesis,
    AUTHOR = "Jiří Weiser",
    TITLE = {Dynamicky rostoucí sdílená hašovací tabulka pro {DiVinE}},
    YEAR = "2013",
    TYPE = "Bakalářská práce",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/374154/fi_b/",
    keywords = {divine}
}

@MastersThesis{Havlicek2013thesis,
    AUTHOR = "Jan Havlíček",
    TITLE = {Untimed {LTL} Model Checking of Timed Automata},
    YEAR = "2013",
    TYPE = "Master's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/324943/fi_m/",
    keywords = {divine}
}

@inproceedings{BHR2013,
	author = {Jiří Barnat and Jan Havlíček and Petr Ročkai},
	booktitle = {Electronic Notes in Theoretical Computer Science, Volume 296},
	doi = {http://dx.doi.org/10.1016/j.entcs.2013.07.006},
	keywords = {model checking; LTL; hash compaction; divine},
	howpublished = {tištěná verze "print"},
	language = {eng},
	location = {Neuveden},
	pages = {79-93},
	publisher = {Elsevier Science},
	title = {Distributed LTL Model Checking with Hash Compaction},
	url = {http://dx.doi.org/10.1016/j.entcs.2013.07.006},
	year = {2013}
}

@InProceedings{BBH+13DIVINE,
    author    = "Jiří Barnat and Luboš Brim and Vojtěch Havel and Jan Havlíček and Jan Kriho and Milan Lenčo and Petr Ročkai and Vladimír Štill and Jiří Weiser",
    title={{DiVinE} 3.0 – An Explicit-State Model Checker for Multithreaded {C} \& {C}++ Programs},
    booktitle={Computer Aided Verification},
    pages     = "863--868",
    volume    = "8044",
    series={LNCS},
    year      = "2013",
    isbn={978-3-642-39798-1},

    editor={Sharygina, Natasha and Veith, Helmut},
    doi={10.1007/978-3-642-39799-8_60},
    publisher={Springer Berlin Heidelberg},
    language={English},
    keywords = {divine}
}

@InProceedings{BBH13LTL,
  author =       "Jiří Barnat and Luboš Brim and Vojtěch Havel",
  title =        {{LTL} Model Checking of Parallel Programs with Under-Approximated {TSO} Memory Model},
  booktitle =    {Application of Concurrency to System Design ({ACSD})},
  pages =        "51--59",
  year =         "2013",
  doi =          "10.1109/ACSD.2013.8",
  publisher =    "IEEE",
  keywords = {divine},
}

@InProceedings{RBB13,
  author =       "Petr Ročkai and Jiří Barnat and Luboš Brim",
  title =        {Improved State Space Reductions for {LTL} Model Checking of {C} \& {C}++ Programs},
  booktitle =    {NASA Formal Methods ({NFM}},
  pages =        "1--15",
  year =         "2013",
  volume =       "7871",
  series =       "LNCS",
  publisher =    "Springer",
  keywords = {divine},
}

@inproceedings{BHB2014,
	author = {Petr Bauch and Vojtěch Havel and Jiří Barnat},
	address = {Telc},
	booktitle = {Proceedings of MEMICS'14},
	doi = {http://dx.doi.org/10.1007/978-3-319-14896-0_5},
	editor = {P. Hlineny et al.},
	keywords = {llvm; formal verification; model checking; divine},
	howpublished = {elektronická verze "online"},
	language = {eng},
	location = {Telc},
	isbn = {978-3-319-14895-3},
	pages = {47-59},
	publisher = {Springer},
	title = {LTL Model Checking of LLVM Bitcode with Symbolic Data},
	year = {2014}
}

@MastersThesis{Havel2014thesis,
    AUTHOR = "Vojtěch Havel",
    TITLE = {Generic Platform for Explicit-Symbolic Verification},
    YEAR = "2014",
    TYPE = "Master's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/359437/fi_m/",
    keywords = {divine}
}

@INPROCEEDINGS{BBH14Input,
   author={Jiří Barnat and Petr Bauch and Vojtěch Havel},
    booktitle={Parallel, Distributed and Network-Based Processing (PDP), 2014
        22nd Euromicro International Conference on},
   title={{Model Checking Parallel Programs with Inputs}},
   year={2014},
   pages={756-759},
   doi={10.1109/PDP.2014.44},
   ISSN={1066-6192},
   month={Feb},
   keywords={computability;parallel programming;program verification;temporal
        logic;LTL model checking;explicit approach;input variables;linear
            temporal logic;noncanonical representations;parallel program model
            checking;parallel program verification;quantified bit-vector
            formulae;quantifier-free satisfiability;state matching;state space
            representation;state space searching;symbolic
            approach;Concrete;Educational institutions;Input variables;Model
            checking;Protocols;Scalability;Standards;bit-vector
            theory;concurrency verification;ltl model checking;satisfiability
            modulo theories, divine}
}

@Article{rockai16:model.checkin,
  pages = {68 -- 85},
  volume = {128},
  year = {2016},
  journal = {Science of Computer Programming},
  title = {Model Checking {C}++ Programs with Exceptions},
  author = {Petr Ročkai and Jiří Barnat and Luboš Brim}
}

@INPROCEEDINGS{rockai14:model.checkin,
  author =       "Petr Ročkai and Jiří Barnat and Luboš Brim",
  title =        {Model Checking {C}++ with Exceptions},
  booktitle=     "Automated Verification of Critical Systems",
  series = {AVoCS 2014},
  year =         "2014",
  doi = {10.14279/tuj.eceasst.70.983},
  keywords = {divine},
}

@inproceedings{SRB14CSDR,
    title={Context-Switch-Directed Verification in {DIVINE}},
    author={Vladimír Štill and Petr Ročkai and Jiří Barnat},
    isbn={978-3-319-14895-3},
    volume={8934},
    pages={135--146},
    year={2014},
    booktitle={Mathematical and Engineering Methods in Computer Science},
    volume={8934},
    series={LNCS},
    editor={Hliněný, Petr and Dvořák, Zdeněk and Jaroš, Jiří and Kofroň, Jan and
        Kořenek, Jan and Matula, Petr and Pala, Karel},
    doi={10.1007/978-3-319-14896-0_12},
    publisher={Springer International Publishing},
    language={English},
    keywords = "divine"
}

@inproceedings{RSB15TC,
  author    = {Petr Ročkai and Vladimír Štill and Jiří Barnat},
  title     = {Techniques for Memory-Efficient Model Checking of {C} and {C}++ Code},
  booktitle = {Software Engineering and Formal Methods},
  pages     = {268--282},
  volume    = {9276},
  year      = {2015},

  isbn={978-3-319-22968-3},
  series={LNCS},
  editor={Calinescu, Radu and Rumpe, Bernhard},
  doi={10.1007/978-3-319-22969-0_19},
  publisher={Springer International Publishing},
  language={English},
  keywords = "divine"
}

@PhdThesis{RockaiPhD,
    AUTHOR = "Petr Ročkai",
    TITLE = "Model Checking Software",
    YEAR = "2015",
    TYPE = "Ph.D. Thesis",
    SCHOOL = "Masaryk University, Faculty of Informatics, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/139761/fi_d/",
    keywords = "divine"
}

@MastersThesis{Lenco2015thesis,
    AUTHOR = "Milan Lenčo",
    TITLE = {Verification of Name Service Cache Daemon with {DIVINE} Model Checker},
    YEAR = "2015",
    TYPE = "Master's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/359883/fi_m/",
    keywords = "divine"
}

@misc{Zakopcanova2015thesis,
    AUTHOR = "Kristína Zákopčanová",
    TITLE = {On Chaining Divine and Prism Model Checkers},
    YEAR = "2015",
    TYPE = "Bachelor's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/390623/fi_b/",
}

@inproceedings{SRB15weakmem,
    author={Vladimír Štill and Petr Ročkai and Jiří Barnat},
    year={2016},
    booktitle={Mathematical and Engineering Methods in Computer Science, Revised Selected Papers},
    editor="Jan Kofroň and Tomáš Vojnar",
    volume={9548},
    series={LNCS},
    title="{Weak Memory Models as LLVM-to-LLVM Transformations}",
    keywords = "divine",
    publisher="Springer International Publishing",
    pages="144--155",
    isbn="978-3-319-29817-7",
    doi="10.1007/978-3-319-29817-7_13"
}

@incollection{BRSW15HS,
    year={2015},
    isbn={978-3-319-23403-8},
    booktitle={Model Checking Software {(SPIN)}},
    volume={9232},
    series={LNCS},
    editor={Fischer, Bernd and Geldenhuys, Jaco},
    doi={10.1007/978-3-319-23404-5_5},
    title={Fast, Dynami\-cally-Sized Concurrent Hash Table},
    publisher={Springer International Publishing},
    author={Jiří Barnat and Petr Ročkai and Vladimír Štill and Jiří Weiser},
    pages={49-65},
    language={English},
    keywords = "divine"
}

@INPROCEEDINGS{BCRSZ16Prob,
    author={Jiří Barnat and Ivana Černá and Petr Ročkai and Vladimír Štill and
        Kristína Zákopčanová},
    title={On Verifying {C}++ Programs with Probabilities},
    year={2016},
    booktitle={{ACM} Symposium on Applied Computing},
    doi={10.1145/2851613.2851721},
    isbn={978-1-4503-3739-7},
    keywords = "divine",
    pages     = {1238--1243},
    crossref  = {DBLP:conf/sac/2016},
    url       = {http://doi.acm.org/10.1145/2851613.2851721},
    biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sac/BarnatCRSZ16},
    bibsource = {dblp computer science bibliography, http://dblp.org}
}

@MastersThesis{Still2016thesis,
    AUTHOR = "Vladimír Štill",
    TITLE = {{LLVM} Transformations for Model Checking},
    YEAR = "2016",
    urldate = "2016-03-01",
    TYPE = "Master's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/373979/fi_m/",
    keywords = "divine"
}

@MastersThesis{Weiser2016thesis,
    AUTHOR = "Jiří Weiser",
    TITLE = {{TCP} vrstva pro verifikační nástroj {DIVINE}},
    YEAR = "2016",
    TYPE = "Diplomová práce",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/374154/fi_m/",
    keywords = "divine"
}

@INPROCEEDINGS{SRB16SVC,
    author={Vladimír Štill and Petr Ročkai and Jiří Barnat},
    title={{DIVINE: Explicit-State LTL Model Checker}},
    year={2016},
    booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
    publisher="Springer Berlin Heidelberg",
    address="Berlin, Heidelberg",
    pages="920--922",
    isbn="978-3-662-49674-9",
    doi="10.1007/978-3-662-49674-9_60",
    url="http://dx.doi.org/10.1007/978-3-662-49674-9_60",
    keywords = "divine"
}

@misc{Mrazek2016thesis,
    AUTHOR = "Jan Mrázek",
    TITLE = {Caching {SMT} Queries in {SymDIVINE}},
    YEAR = "2016",
    TYPE = "Bachelor's Thesis",
    SCHOOL = "Masarykova univerzita, Fakulta informatiky, Brno",
    SUPERVISOR = "Jiří Barnat",
    URL = "http://is.muni.cz/th/422279/fi_b/",
    keywords = {divine,symdivine}
}

@InProceedings{MBLB2016,
    author="Jan Mrázek and Petr Bauch and Henrich Lauko and Jiří Barnat",
    editor="Bošnački, Dragana and Wijs, Anton",
    title={{SymDIVINE}: Tool for Control-Explicit Data-Symbolic State Space Exploration},
    bookTitle={Model Checking Software: 23rd International Symposium ({SPIN})},
    year="2016",
    publisher="Springer International Publishing",
    address="Cham",
    pages="208--213",
    isbn="978-3-319-32582-8",
    doi="10.1007/978-3-319-32582-8_14",
    url="http://dx.doi.org/10.1007/978-3-319-32582-8_14",
    keywords = {divine,symdivine}
}

@Article{rockai18:divm,
    url = {https://divine.fi.muni.cz/2017/divm},
    year = {2018},
    title = {{DiVM}: Model Checking with {LLVM} and Graph Memory},
    author = {Petr Ročkai and Vladimír Štill and Ivana Černá and Jiří Barnat},
    doi = {10.1016/j.jss.2018.04.026},
    journal = {Journal of Systems and Software},
    pages = {1--13},
    publisher = {Elsevier},
    volume = {143}
}

@Article{rockai17:simulat.llvm.bitcod,
    author    = {Petr Ročkai and Jiří Barnat},
    title     = {A Simulator for {LLVM} Bitcode},
    journal   = {CoRR},
    volume    = {abs/1704.05551},
    year      = {2017},
    url       = {https://divine.fi.muni.cz/2017/sim},
    archivePrefix = {arXiv},
    eprint    = {1704.05551},
}

@InProceedings{still17:using.off,
    author = {Vladimír Štill and Petr Ročkai and Jiří Barnat},
    title = {Using Off-the-Shelf Exception Support Components in {C}++ Verification},
    booktitle = {{IEEE} International Conference on Software Quality, Reliability and Security (QRS)},
    year = {2017},
    pages = {54-64},
    url = {https://divine.fi.muni.cz/2017/exceptions},
}

@InProceedings{baranova17:model.checkin,
    author = {Zuzana Baranová and Jiří Barnat and Katarína Kejstová
            and Tadeáš Kučera and Henrich Lauko and Jan Mrázek
            and Petr Ročkai and Vladimír Štill},
    title = {Model Checking of {C} and {C}++ with {DIVINE} 4},
    booktitle = {Automated Technology for Verification and Analysis, {ATVA}},
    pages     = {201-207},
    volume = {10482},
    series = {LNCS},
    year = {2017},
    publisher = {Springer},
    url = {https://divine.fi.muni.cz/2017/divine4},
}

@InProceedings{kejstova17:from.model,
    author    = {Katarína Kejstová and Petr Ročkai and Jiří Barnat},
    title     = {From Model Checking to Runtime Verification and Back},
    booktitle = {Runtime Verification - 17th International Conference, {RV} 2017},
    pages     = {225--240},
    year      = {2017},
    url       = {https://divine.fi.muni.cz/2017/passthrough},
}

@MastersThesis{kejstova19:model.checking.system,
  author     = "Katarína Kejstová",
  title      = "Model Checking with System Call Traces",
  year       = "2019",
  type       = "Master's Thesis",
  school     = "Masarykova univerzita, Fakulta informatiky, Brno",
  supervisor = "Petr Ročkai",
  url        = "http://is.muni.cz/th/tukvk/"
}

@inproceedings{rockai19:reproduc.execution,
  author = {Petr Ročkai and Zuzana Baranová and Jan Mrázek and Katarína Kejstová and Jiří Barnat},
  title = {Reproducible Execution of {POSIX} Programs with {DiOS}},
  booktitle = {Software Engineering and Formal Methods},
  year = {2019},
  series = {LNCS},
  publisher = {Springer},
  language = {English},
  url = {https://divine.fi.muni.cz/2019/dios/}
}

@InProceedings{rockai19:sim,
  author="Ročkai, Petr
  and Barnat, Jiří",
  title="A Simulator for {LLVM} Bitcode",
  booktitle="Formal Methods for Industrial Critical Systems",
  year="2019",
  publisher="Springer",
  address="Cham",
  pages="127--142"
}

@inproceedings{lauko18:symbolic.computation,
author={Lauko, H. and Ročkai, P. and Barnat, J.},
title={Symbolic Computation via Program Transformation},
year={2018},
volume={11187 LNCS},
pages={313-332},
doi={10.1007/978-3-030-02508-3_17},
url={https://divine.fi.muni.cz/2018/sym/}
}

@ARTICLE{lauko20:abstracting.strings,
author={Lauko, H. and Olliaro, M. and Cortesi, A. and Ročkai, P.},
title={Abstracting strings for model checking of {C} programs},
journal={Applied Sciences (Switzerland)},
year={2020},
volume={10},
number={21},
pages={1-33},
doi={10.3390/app10217853},
art_number={7853},
note={cited By 0},
url={https://divine.fi.muni.cz/2020/mstring/}
}

@ARTICLE{rockai20:model.checking,
author={Ročkai, P.},
title={Model checking in a development workflow: A study on a concurrent {C}++ hash table},
booktitle={3rd World Congress on Formal Methods, {FM} 2019},
year={2020},
volume={12232 LNCS},
pages={46-60},
doi={10.1007/978-3-030-54994-7_5},
url={https://divine.fi.muni.cz/2019/hash}
}

@ARTICLE{baranova20:compiling.programs,
author={Baranová, Z. and Ročkai, P.},
title={Compiling {C} and {C}++ programs for dynamic white-box analysis},
booktitle={3rd World Congress on Formal Methods, {FM} 2019},
year={2020},
volume={12232 LNCS},
pages={30-45},
doi={10.1007/978-3-030-54994-7_4},
url={https://divine.fi.muni.cz/2019/divcc/}
}

@inproceedings{cortesi19:string.abstraction,
author={Cortesi, A. and Lauko, H. and Olliaro, M. and Ročkai, P.},
title={String Abstraction for Model Checking of {C} Programs},
booktitle={Model Checking Software ({SPIN})},
year={2019},
volume={11636 LNCS},
pages={74-93},
doi={10.1007/978-3-030-30923-7_5},
url={https://divine.fi.muni.cz/2019/mstring/}
}

@inproceedings{lauko19:extending.divine,
author={Lauko, H. and Štill, V. and Ročkai, P. and Barnat, J.},
title={Extending DIVINE with Symbolic Verification Using SMT: (Competition Contribution)},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
year={2019},
volume={11429 LNCS},
pages={204-208},
doi={10.1007/978-3-030-17502-3_14},
url={https://divine.fi.muni.cz/2019/sv-comp-smt/}
}


@inproceedings{korencik20:symbolic.execution,
author={Korencik, L. and Rockai, P. and Lauko, H. and Barnat, J.},
title={On Symbolic Execution of Decompiled Programs},
booktitle={International Conference on Software Quality, Reliability, and Security},
year={2020},
pages={265-272},
doi={10.1109/QRS51102.2020.00044},
art_number={9282790},
url={https://divine.fi.muni.cz/2020/decompile},
document_type={Conference Paper},
source={Scopus},
}


@article{rockai21:dios,
  author = {Ročkai, Petr and Baranová, Zuzana and Mrázek, Jan and Kejstová, Katarína and Barnat, Jiří},
  year = {2021},
  volume = {20},
  pages = {363-382},
  title = {Reproducible execution of {POSIX} programs with {DiOS}},
  journal = {Software and Systems Modeling},
  doi = {10.1007/s10270-020-00837-y},
  url = {https://divine.fi.muni.cz/2020/dios/}
}

@inproceedings{SB2018x86tso,
    author = {Vladimír Štill and Jiří Barnat},
    booktitle = {Formal Methods and Software Engineering},
    editor = {Sun, Jing and Sun, Meng},
    isbn = {978-3-030-02450-5},
    keywords = {divine},
    pages = {124--140},
    publisher = {Springer International Publishing},
    title = {{Model Checking of C++ Programs Under the x86-TSO Memory Model}},
    url = {https://divine.fi.muni.cz/2018/x86tso},
    year = {2018}
}

@ARTICLE{rockai22:divsim,
  author={Ročkai, P. and Barnat, J.},
  title={{DivSIM}, an interactive simulator for {LLVM} bitcode},
  journal={International Journal on Software Tools for Technology Transfer},
  year={2022},
  doi={10.1007/s10009-022-00659-x},
  url={https://divine.fi.muni.cz/2021/sim}
}

@inproceedings{lauko22:lart,
author={Lauko, H. and Ročkai, P.},
title={{LART}: Compiled Abstract Execution: (Competition Contribution)},
year={2022},
booktitle={Tools and Algorithms for the Construction and Analysis of Software},
volume={13244 LNCS},
pages={457-461},
doi={10.1007/978-3-030-99527-0_31},
url={https://divine.fi.muni.cz/2022/lart}
}