Parosh Aziz Abdulla, Lisa Kaati & Johanna Högberg (2006):
Bisimulation Minimization of Tree Automata.
In: CIAA,
Lecture Notes in Computer Science 4094.
Springer,
pp. 173–185,
doi:10.1137/0216062.
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds & Cesare Tinelli (2011):
CVC4.
In: CAV,
Lecture Notes in Computer Science 6806.
Springer,
pp. 171–177,
doi:10.1007/3-540-45657-0_40.
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015):
Horn Clause Solvers for Program Verification.
In: Fields of Logic and Computation II,
Lecture Notes in Computer Science 9300.
Springer,
pp. 24–51,
doi:10.1007/978-3-319-19249-9.
Jürgen Christ, Jochen Hoenicke & Alexander Nutz (2012):
SMTInterpol: An Interpolating SMT Solver.
In: SPIN,
Lecture Notes in Computer Science 7385.
Springer,
pp. 248–254,
doi:10.1007/11532231_26.
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma & Roberto Sebastiani (2013):
The MathSAT5 SMT Solver.
In: TACAS,
Lecture Notes in Computer Science 7795.
Springer,
pp. 93–107,
doi:10.1007/978-3-642-31365-3_38.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu & Helmut Veith (2000):
Counterexample-Guided Abstraction Refinement.
In: CAV,
Lecture Notes in Computer Science 1855.
Springer,
pp. 154–169,
doi:10.1007/3-540-49519-3_18.
H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison & M. Tommasi (2007):
Tree Automata Techniques and Applications.
Available on: http://www.grappa.univ-lille3.fr/tata.
Release October, 12th 2007.
Daniel Dietsch, Matthias Heizmann, Betim Musa, Alexander Nutz & Andreas Podelski (2017):
Craig vs. Newton in software model checking.
In: ESEC/SIGSOFT FSE.
ACM,
pp. 487–497,
doi:10.1145/3106237.3106307.
Niklas Eén, Alan Mishchenko & Robert K. Brayton (2011):
Efficient implementation of property directed reachability.
In: FMCAD.
FMCAD Inc.,
pp. 125–134.
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012):
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution).
In: TACAS,
Lecture Notes in Computer Science 7214.
Springer,
pp. 549–551,
doi:10.1007/978-3-540-69611-7_16.
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, Jochen Hoenicke & Andreas Podelski (2009):
Refinement of Trace Abstraction.
In: SAS,
Lecture Notes in Computer Science 5673.
Springer,
pp. 69–85,
doi:10.1007/978-3-540-73368-3_46.
Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2010):
Nested interpolants.
In: POPL.
ACM,
pp. 471–482,
doi:10.1145/1706299.1706353.
Jochen Hoenicke, Rupak Majumdar & Andreas Podelski (2017):
Thread modularity at many levels: a pearl in compositional verification.
In: POPL.
ACM,
pp. 473–485,
doi:10.1145/3009837.3009893.
Bishoksan Kafle & John P. Gallagher (2015):
Tree Automata-Based Refinement with Application to Horn Clause Verification.
In: VMCAI,
Lecture Notes in Computer Science 8931.
Springer,
pp. 209–226,
doi:10.1007/3-540-52753-2_52.
Bishoksan Kafle, John P. Gallagher & José F. Morales (2016):
Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata.
In: CAV (1),
Lecture Notes in Computer Science 9779.
Springer,
pp. 261–268,
doi:10.1016/j.jsc.2010.06.005.
Leonardo Mendonça de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: TACAS,
Lecture Notes in Computer Science 4963.
Springer,
pp. 337–340,
doi:10.1109/MS.2006.117.
Weifeng Wang & Li Jiao (2016):
Trace Abstraction Refinement for Solving Horn Clauses.
Comput. J. 59(8),
pp. 1236–1251,
doi:10.1145/69575.69577.
eptcs@eptcs.org