@article(chc-comp_report22,
 author       = {Emanuele~De Angelis and Hari Govind~V K},
 year         = {2022},
 title        = {{CHC}-{COMP} 2022: Competition Report},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {373},
 pages        = {44--62},
 doi          = {10.4204/eptcs.373.5},
)
@inproceedings(formalise,
 author       = {Levente Bajczi and Zsófia Ádám and Vince Molnár},
 year         = {2022},
 title        = {{C for Yourself: Comparison of Front-End Techniques for Formal Verification}},
 booktitle    = {2022 IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE)},
 doi          = {10.1145/3524482.3527646},
)
@inproceedings(boogie,
 author       = {Mike Barnett and Bor-Yuh~Evan Chang and Robert DeLine and Bart Jacobs and K.~Rustan~M. Leino},
 year         = {2006},
 title        = {Boogie: A Modular Reusable Verifier for Object-Oriented Programs},
 editor       = {Frank~S. de~Boer and Marcello~M. Bonsangue and Susanne Graf and Willem-Paul de~Roever},
 booktitle    = {Formal Methods for Components and Objects},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {364--387},
 doi          = {10.1007/11804192_17},
)
@article(cegar,
 author       = {Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2003},
 title        = {Counterexample-Guided Abstraction Refinement for Symbolic Model Checking},
 journal      = {J. ACM},
 volume       = {50},
 number       = {5},
 pages        = {752–794},
 doi          = {10.1145/876638.876643},
)
@article(clarke_klieber_novacek_zuliani_2012,
 author       = {Edmund~M. Clarke and William Klieber and Miloš Nováček},
 year         = {2012},
 title        = {{Model checking and the state explosion problem}},
 journal      = {Lecture Notes in Computer Science},
 pages        = {1–30},
 doi          = {10.1007/978-3-642-35746-6_1},
)
@inproceedings(tricera,
 author       = {Zafer Esen and Philipp Ruemmer},
 year         = {2022},
 title        = {TRICERA: Verifying C Programs Using the Theory of Heaps},
 booktitle    = {CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN--FMCAD 2022},
 publisher    = {TU Wien Academic Press},
 pages        = {360--391},
 doi          = {10.34727/2022/isbn.978-3-85448-053-2_45},
)
@inproceedings(chccomp21,
 author       = {Grigory Fedyukovich and Philipp R{\"{u}}mmer},
 year         = {2021},
 title        = {Competition Report: {CHC-COMP-21}},
 editor       = {Hossein Hojjat and Bishoksan Kafle},
 booktitle    = {Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021},
 series       = {{EPTCS}},
 volume       = {344},
 pages        = {91--108},
 doi          = {10.4204/EPTCS.344.7},
)
@book(clarke_grumberg_peled_1999,
 author       = {Orna Grumberg and Doron~A Peled and EM~Clarke},
 year         = {1999},
 title        = {{Model checking}},
 publisher    = {MIT press Cambridge},
)
@inproceedings(spacer,
 author       = {Arie Gurfinkel},
 year         = {2022},
 title        = {Program Verification with Constrained Horn Clauses (Invited Paper)},
 editor       = {Sharon Shoham and Yakir Vizel},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {19--29},
 doi          = {10.1007/978-3-031-13185-1_2},
)
@inproceedings(seahorn,
 author       = {Arie Gurfinkel and Temesghen Kahsai and Anvesh Komuravelli and Jorge~A. Navas},
 year         = {2015},
 title        = {The SeaHorn Verification Framework},
 editor       = {Daniel Kroening and Corina~S. Păsăreanu},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {343--361},
 doi          = {10.1007/978-3-319-21690-4_20},
)
@article(theta,
 author       = {Ákos Hajdu and Zoltán Micskei},
 year         = {2020},
 title        = {Efficient Strategies for CEGAR-Based Model Checking},
 journal      = {Journal of Automated Reasoning},
 volume       = {64},
 number       = {6},
 pages        = {1051--1091},
 doi          = {10.1007/s10817-019-09535-x},
)
@inproceedings(automizer,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2009},
 title        = {Refinement of Trace Abstraction},
 editor       = {Jens Palsberg and Zhendong Su},
 booktitle    = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5673},
 publisher    = {Springer},
 pages        = {69--85},
 doi          = {10.1007/978-3-642-03237-0\_7},
)
@inproceedings(eldarica,
 author       = {Hossein Hojjat and Philipp Rümmer},
 year         = {2018},
 title        = {The ELDARICA Horn Solver},
 booktitle    = {2018 Formal Methods in Computer Aided Design (FMCAD)},
 pages        = {1--7},
 doi          = {10.23919/FMCAD.2018.8603013},
)
@article(rusthorn,
 author       = {Yusuke Matsushita and Takeshi Tsukada and Naoki Kobayashi},
 year         = {2021},
 title        = {RustHorn: CHC-Based Verification for Rust Programs},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {43},
 number       = {4},
 doi          = {10.1145/3462205},
)
@inproceedings(z3,
 author       = {Leonardo de~Moura and Nikolaj Bjørner},
 year         = {2008},
 title        = {Z3: An Efficient SMT Solver},
 editor       = {C.~R. Ramakrishnan and Jakob Rehof},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@book(antlr,
 author       = {Terence Parr},
 year         = {2013},
 title        = {The Definitive ANTLR 4 Reference},
 publisher    = {Pragmatic Bookshelf},
 doi          = {10.5555/2501720},
)
@article(turing1936computable,
 author       = {A.~M. Turing},
 year         = {1937},
 title        = {On Computable Numbers, with an Application to the Entscheidungsproblem},
 journal      = {Proceedings of the London Mathematical Society},
 volume       = {s2-42},
 number       = {1},
 pages        = {230--265},
 doi          = {10.1112/plms/s2-42.1.230},
)
@inproceedings(datalog_bottomup,
 author       = {Jeffrey~D. Ullman},
 year         = {1989},
 title        = {Bottom-Up Beats Top-Down for Datalog},
 editor       = {Avi Silberschatz},
 booktitle    = {Proceedings of the Eighth {ACM} {SIGACT-SIGMOD-SIGART} Symposium on Principles of Database Systems, March 29-31, 1989, Philadelphia, Pennsylvania, {USA}},
 publisher    = {{ACM} Press},
 pages        = {140--149},
 doi          = {10.1145/73721.73736},
)