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