Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015):
Horn Clause Solvers for Program Verification.
In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday,
pp. 24–51,
doi:10.1007/978-3-319-23534-9_2.
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz & Andreas Podelski (2019):
Ultimate TreeAutomizer (CHC-COMP Tool Description).
In: HCVS/PERR@ETAPS,
EPTCS 296,
pp. 42–47,
doi:10.4204/EPTCS.296.7.
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012):
Synthesizing Software Verifiers from Proof Rules.
In: PLDI.
ACM,
pp. 405–416,
doi:10.1145/2254064.2254112.
Arie Gurfinkel, Sharon Shoham & Yakir Vizel (2018):
Quantifiers on Demand.
In: Shuvendu K. Lahiri & Chao Wang: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings,
Lecture Notes in Computer Science 11138.
Springer,
pp. 248–266,
doi:10.1007/978-3-030-01090-4_15.
Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler & Andreas Podelski (2018):
Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution).
In: TACAS (2),
LNCS 10806.
Springer,
pp. 447–451,
doi:10.1007/978-3-319-89963-3_30.
Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2013):
Software Model Checking for People Who Love Automata.
In: CAV,
LNCS 8044.
Springer,
pp. 36–52,
doi:10.1007/978-3-642-39799-8_2.
Jochen Hoenicke & Tanja Schindler (2018):
Efficient Interpolation for the Theory of Arrays.
In: IJCAR,
LNCS 10900.
Springer,
pp. 549–565,
doi:10.1007/978-3-319-94205-6_36.
Hossein Hojjat & Philipp Rümmer (2018):
The ELDARICA Horn Solver.
In: Nikolaj Bjørner & Arie Gurfinkel: 2018 Formal Methods in Computer Aided Design, FMCAD.
IEEE,
pp. 1–7,
doi:10.23919/FMCAD.2018.8603013.
Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt & Natasha Sharygina (2016):
OpenSMT2: An SMT Solver for Multi-core and Cloud Computing.
In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings,
Lecture Notes in Computer Science 9710.
Springer,
pp. 547–553,
doi:10.1007/978-3-319-40970-2_35.
Hari Govind V K, YuTing Chen, Sharon Shoham & Arie Gurfinkel (2020):
Global Guidance for Local Generalization in Model Checking.
In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II,
Lecture Notes in Computer Science 12225.
Springer,
pp. 101–125,
doi:10.1007/978-3-030-53291-8_7.
Hari Govind V. K., Grigory Fedyukovich & Arie Gurfinkel (2020):
Word Level Property Directed Reachability.
In: IEEE/ACM International Conference On Computer Aided Design, ICCAD 2020, San Diego, CA, USA, November 2-5, 2020.
IEEE,
pp. 107:1–107:9,
doi:10.1145/3400302.3415708.
Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2016):
SMT-based Model Checking for Recursive Programs.
Formal Methods Syst. Des. 48(3),
pp. 175–205,
doi:10.1007/s10703-016-0249-4.
Yurii Kostyukov, Dmitry Mordvinov & Grigory Fedyukovich (2021):
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types.
In: PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211.
ACM,
pp. 451–465,
doi:10.1145/3453483.3454055.
Satoshi Kura, Hiroshi Unno & Ichiro Hasuo (2021):
Decision Tree Learning in CEGIS-Based Termination Analysis.
In: Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II,
Lecture Notes in Computer Science 12760.
Springer,
pp. 75–98,
doi:10.1007/978-3-030-81688-9_4.
Kenneth L. McMillan (2006):
Lazy Abstraction with Interpolants.
In: Thomas Ball & Robert B. Jones: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings,
Lecture Notes in Computer Science 4144.
Springer,
pp. 123–136,
doi:10.1007/11817963_14.
Andrew Reynolds, Cesare Tinelli, Amit Goel & Sava Krsti\'c (2013):
Finite model finding in SMT.
In: International Conference on Computer Aided Verification,
Lecture Notes in Computer Science 8044.
Springer,
pp. 640–655,
doi:10.1007/978-3-642-39799-8_42.
Philipp Rümmer (2008):
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.
In: Proceedings, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning,
LNCS 5330.
Springer,
pp. 274–289,
doi:10.1007/978-3-540-89439-1_20.
Philipp Rümmer (2020):
Competition Report: CHC-COMP-20.
In: Laurent Fribourg & Matthias Heizmann: Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT/HCVS@ETAPS 2020, Dublin, Ireland, 25-26th April 2020,
EPTCS 320,
pp. 197–219,
doi:10.4204/EPTCS.320.15.
Yuki Satake, Hiroshi Unno & Hinata Yanagi (2020):
Probabilistic Inference for Predicate Constraint Satisfaction.
In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020.
AAAI Press,
pp. 1644–1651,
doi:10.1609/aaai.v34i02.5526.
Aaron Stump, Geoff Sutcliffe & Cesare Tinelli (2014):
StarExec: A Cross-Community Infrastructure for Logic Solving.
In: Stéphane Demri, Deepak Kapur & Christoph Weidenbach: Automated Reasoning - 7th International Joint Conference, IJCAR,
LNCS 8562.
Springer,
pp. 367–373,
doi:10.1007/978-3-319-08587-6_28.
Hiroshi Unno, Tachio Terauchi & Eric Koskinen (2021):
Constraint-based Relational Verification.
In: Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I,
Lecture Notes in Computer Science 12759.
Springer,
pp. 742–766,
doi:10.1007/978-3-030-81685-8_35.