References

  1. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016): The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org.
  2. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan & Andrey Rybalchenko (2015): Horn Clause Solvers for Program Verification. In: Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner & Wolfram Schulte: Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Springer International Publishing, Cham, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
  3. Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen & Natasha Sharygina (2022): Transition Power Abstractions for Deep Counterexample Detection. In: Dana Fisman & Grigore Rosu: Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, pp. 524–542, doi:10.1007/978-3-030-99524-9_29.
  4. Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi & Maurizio Proeitti (2021): Analysis and Transformation of Constrained Horn Clauses for Program Verification. Theory and Practice of Logic Programming, pp. 1–69, doi:10.1017/S1471068421000211.
  5. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2022): Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach. J. Log. Comput. 32(2), pp. 402–442, doi:10.1093/logcom/exab090.
  6. 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.
  7. 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. Open Publishing Association, pp. 91–108, doi:10.4204/EPTCS.344.7.
  8. 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.
  9. 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), Lecture Notes in Computer Science 10806. Springer, pp. 447–451, doi:10.1007/978-3-319-89963-3_30.
  10. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2013): Software Model Checking for People Who Love Automata. In: CAV, Lecture Notes in Computer Science 8044. Springer, pp. 36–52, doi:10.1007/978-3-642-39799-8_2.
  11. Jochen Hoenicke & Tanja Schindler (2018): Efficient Interpolation for the Theory of Arrays. In: IJCAR, Lecture Notes in Computer Science 10900. Springer, pp. 549–565, doi:10.1007/978-3-319-94205-6_36.
  12. 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.
  13. Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt & Natasha Sharygina (2016): OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. In: Nadia Creignou & Daniel Le Berre: Theory and Applications of Satisfiability Testing – SAT 2016. Springer International Publishing, Cham, pp. 547–553, doi:10.1007/978-3-319-40970-2_35.
  14. Hari Govind V. K., Sharon Shoham & Arie Gurfinkel (2022): Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), pp. 1–29, doi:10.1145/3498722.
  15. Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2016): SMT-based Model Checking For Recursive Programs. Formal Methods in System Design 48(3), pp. 175–205, doi:10.1007/s10703-016-0249-4.
  16. Yurii Kostyukov, Dmitry Mordvinov & Grigory Fedyukovich (2021): Beyond the Elementary Representations of Program Invariants over Algebraic Data Types. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021. ACM, pp. 451–465, doi:10.1145/3453483.3454055.
  17. Kenneth L. McMillan (2006): Lazy Abstraction with Interpolants. In: Thomas Ball & Robert B. Jones: Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 123–136, doi:10.1007/11817963_14.
  18. Alexandre Riazanov & Andrei Voronkov (2002): The Design and Implementation of VAMPIRE. AI Commun. 15(2,3), pp. 91–110.
  19. 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.
  20. 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. Springer International Publishing, Cham, pp. 367–373, doi:10.1007/978-3-319-08587-6_28.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org