References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. N. D. Jones, C. Gomard & P. Sestoft (1993): Partial Evaluation and Automatic Software Generation. Prentice Hall, doi:10.1016/j.scico.2004.03.010.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. D. Sahlin (1993): Mixtus: An Automatic Partial Avaluator for Full Prolog. New Generation Comput. 12(1), pp. 7–51, doi:10.1007/BF03038271.
  26. 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.
  27. 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.
  28. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org