@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 (HiBi/PDMC 2010)}",
  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 2010)}",
  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 2013)}",
  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}
}

@INPROCEEDINGS{RBB14Exc,
  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 2015)},
    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},
    note = {Preliminary version},
    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 2017)},
    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},
}

@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}
}