T. Ball, A. Podelski & S. K. Rajamani (2001):
Boolean and Cartesian Abstraction for Model Checking C Programs.
In: T. Margaria & W. Yi: Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001, Proceedings,
Lecture Notes in Computer Science 2031.
Springer,
pp. 268–283,
doi:10.1007/3-540-45319-9_19.
K. Benkerimi & J. W. Lloyd (1990):
A Partial Evaluation Procedure for Logic Programs.
In: S. K. Debray & M. V. Hermenegildo: Logic Programming, Proceedings of the 1990 North American Conference.
MIT Press,
pp. 343–358.
N. Bjørner, A. Gurfinkel, K. L. McMillan & A. Rybalchenko (2015):
Horn Clause Solvers for Program Verification.
In: L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeiner & W. Schulte: Fields of Logic and Computation II,
LNCS 9300.
Springer,
pp. 24–51,
doi:10.1007/978-3-319-23534-9_2.
P. Cousot & R. Cousot (1977):
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles,
pp. 238–252,
doi:10.1145/512950.512973.
P. Cousot & R. Cousot (1992):
Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation.
In: 4th International Symposium on Programming Language Implementation and Logic Programming,
Springer-Verlag Lecture Notes in Computer Science 631,
pp. 269–295,
doi:10.1007/3-540-55844-6_142.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2012):
Specialization with Constrained Generalization for Software Model Checking.
In: E. Albert: LOPSTR 2012,
Lecture Notes in Computer Science 7844.
Springer,
pp. 51–70,
doi:10.1007/978-3-642-38197-3_5.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
Program verification via iterated specialization.
Sci. Comput. Program. 95,
pp. 149–175,
doi:10.1016/j.scico.2014.05.017.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018):
Predicate Pairing for program verification.
TPLP 18(2),
pp. 126–166,
doi:10.1017/S1471068417000497.
J. Doménech, S. Genaim & J. P. Gallagher (2018):
Control-Flow Refinement via Partial Evaluation.
In: S. Lucas: 16th International Workshop on Termination (WST 2018),
pp. 55–59.
Available at http://wst2018.webs.upv.es/wst2018proceedings.pdf.
S. Etalle & M. Gabbrielli (1996):
Transformations of CLP Modules.
Theoretical Computer Science 166,
pp. 101–146,
doi:10.1016/0304-3975(95)00148-4.
F. Fioravanti, A. Pettorossi, M. Proietti & V. Senni (2013):
Controlling Polyvariance for Specialization-based Verification.
Fundam. Inform. 124(4),
pp. 483–502,
doi:10.3233/FI-2013-845.
J. P. Gallagher (1993):
Specialisation of Logic Programs: A Tutorial.
In: Proceedings PEPM'93, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation.
ACM Press,
Copenhagen,
pp. 88–98,
doi:10.1145/154630.154640.
J. P. Gallagher & L. Lafave (1996):
Regular Approximation of Computation Paths in Logic and Functional Languages.
In: O. Danvy, R. Glück & P. Thiemann: Partial Evaluation,
Springer-Verlag Lecture Notes in Computer Science 1110,
pp. 115–136,
doi:10.1007/3-540-61580-6_7.
J. P. Gallagher & J. C. Peralta (2001):
Regular Tree Languages as an Abstract Domain in Program Specialisation.
Higher-Order and Symbolic Computation 14(2-3),
pp. 143–172,
doi:10.1023/A:1012936614361.
S. Grebenshchikov, N. P. Lopes, C. Popeea & A. Rybalchenko (2012):
Synthesizing software verifiers from proof rules.
In: J. Vitek, H. Lin & F. Tip: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12.
ACM,
pp. 405–416,
doi:10.1145/2254064.2254112.
S. Gulwani, S. Jain & E. Koskinen (2009):
Control-flow refinement and progress invariants for bound analysis.
In: M. Hind & A. Diwan: PLDI 2009.
ACM,
pp. 375–385,
doi:10.1145/1542476.1542518.
N. D. Jones, C. Gomard & P. Sestoft (1993):
Partial Evaluation and Automatic Software Generation.
Prentice Hall,
doi:10.1016/j.scico.2004.03.010.
B. Kafle, J. P. Gallagher, G. Gange, P. Schachte, H. Søndergaard & P. J. Stuckey (2018):
An iterative approach to precondition inference using constrained Horn clauses.
TPLP 18(3-4),
pp. 553–570,
doi:10.1017/S1471068418000091.
B. Kafle, J. P. Gallagher & P. Ganty (2018):
Tree dimension in verification of constrained Horn clauses.
TPLP 18(2),
pp. 224–251,
doi:10.1017/S1471068418000030.
M. Leuschel & B. Martens (1996):
Global Control for Partial Deduction through Characteristic Atoms and Global Trees.
In: O. Danvy, R. Glück & P. Thiemann: Partial Evaluation,
Springer-Verlag Lecture Notes in Computer Science 1110,
pp. 263–283,
doi:10.1007/3-540-61580-6_13.
M. Leuschel & T. Massart (2000):
Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
In: A. Bossi: Logic-Based Program Synthesis and Transformation (LOPSTR'99),
Springer-Verlag Lecture Notes in Computer Science 1817,
pp. 63–82,
doi:10.1007/10720327_5.
J. Lloyd & J. Shepherdson (1991):
Partial Evaluation in Logic Programming.
Journal of Logic Programming 11(3 & 4),
pp. 217–242,
doi:10.1016/0743-1066(91)90027-M.
B. Martens & J. P. Gallagher (1995):
Ensuring Global Termination of Partial Deduction While Allowing Flexible Polyvariance.
In: L. Sterling: Proc. International Conference on Logic Programming, (ICLP'95), Tokyo.
MIT Press.
A. Pettorossi & M. Proietti (1999):
Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs..
J. Log. Program. 41(2-3),
pp. 197–230,
doi:10.1016/S0743-1066(99)00029-1.
D. Sahlin (1993):
Mixtus: An Automatic Partial Avaluator for Full Prolog.
New Generation Comput. 12(1),
pp. 7–51,
doi:10.1007/BF03038271.
R. Sharma, I. Dillig, T. Dillig & A. Aiken (2011):
Simplifying Loop Invariant Generation Using Splitter Predicates.
In: G. Gopalakrishnan & S. Qadeer: Computer Aided Verification, CAV 2011,
Lecture Notes in Computer Science 6806.
Springer,
pp. 703–719,
doi:10.1007/978-3-642-22110-1_57.
V. Turchin (1988):
The Algorithm of generalization in the supercompiler.
In: D. Bjørner, A. Ershov & N. Jones: Proc. of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation.
North-Holland,
pp. 531–549.
D. de Waal & J. P. Gallagher (1994):
The Applicability of Logic Program Analysis and Transformation to Theorem Proving.
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), Nancy,
doi:10.1007/3-540-58156-1_15.