Armin Biere, Alessandro Cimatti, Edmund Clarke & Yunshan Zhu (1999):
Symbolic Model Checking without BDDs.
In: W. Rance Cleaveland: Tools and Algorithms for the Construction and Analysis of Systems.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 193–207,
doi:10.1007/3-540-49059-0_14.
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.
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofroň & Natasha Sharygina (2019):
Decomposing Farkas Interpolants.
In: Tomáš Vojnar & Lijun Zhang: Tools and Algorithms for the Construction and Analysis of Systems.
Springer International Publishing,
Cham,
pp. 3–20,
doi:10.1007/978-3-030-17462-0_1.
Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti & Natasha Sharygina (2020):
A Cooperative Parallelization Approach for Property-Directed k-Induction.
In: Dirk Beyer & Damien Zufferey: Verification, Model Checking, and Abstract Interpretation.
Springer International Publishing,
Cham,
pp. 270–292,
doi:10.1007/978-3-030-39322-9_13.
Aaron R. Bradley (2011):
SAT-Based Model Checking without Unrolling.
In: VMCAI,
LNCS 6538.
Springer,
pp. 70–87,
doi:10.1007/978-3-642-18275-4_7.
Alessandro Cimatti, Alberto Griggio, Sergio Mover & Stefano Tonetta (2016):
Infinite-state invariant checking with IC3 and predicate abstraction.
Formal Methods Syst. Des. 49(3),
pp. 190–218,
doi:10.1007/s10703-016-0257-4.
Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma & Roberto Sebastiani (2013):
The MathSAT5 SMT Solver.
In: Nir Piterman & Scott Smolka: Proceedings of TACAS,
LNCS 7795.
Springer,
doi:10.1007/978-3-642-36742-7_7.
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.
Bruno Dutertre (2014):
Yices 2.2.
In: Armin Biere & Roderick Bloem: Computer-Aided Verification (CAV'2014),
LNCS 8559.
Springer,
pp. 737–744,
doi:10.1007/978-3-319-08867-9_49.
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.
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: 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.
Dejan Jovanovi\'c & Bruno Dutertre (2016):
Property-directed k-induction.
In: 2016 Formal Methods in Computer-Aided Design (FMCAD),
pp. 85–92,
doi:10.1109/FMCAD.2016.7886665.
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.
To appear.
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.
Daniel Kroening, Alex Groce & Edmund M. Clarke (2004):
Counterexample Guided Abstraction Refinement Via Program Execution.
In: ICFEM,
LNCS 3308.
Springer,
pp. 224–238,
doi:10.1007/978-3-540-30482-1_23.
Matteo Marescotti, Antti Hyv\ "arinen & Natasha Sharygina (2018):
SMTS: Distributed, Visualized Constraint Solving.
In: Gilles Barthe, Geoff Sutcliffe & Margus Veanes: LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning,
EPiC Series in Computing 57.
EasyChair,
pp. 534–542,
doi:10.29007/fhgn.
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.
Yuki Satake, Hiroshi Unno & Hinata Yanagi (2020):
Probabilistic Inference for Predicate Constraint Satisfaction.
In: Proceedings of AAAI 2020.
To appear.
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.
Xiaozhen Zhang & Weiqiang Kong (2020):
Facilitating CHC Solving with Improving Interpolation Abstraction Exploration.
To appear.