References

  1. 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.
  2. S. Blazy & X. Leroy (2009): Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reasoning 43(3), pp. 263–288, doi:10.1007/s10817-009-9148-3.
  3. 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.
  4. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2015): Semantics-based generation of verification conditions by program specialization. In: M. Falaschi & E. Albert: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015. ACM, pp. 91–102, doi:10.1145/2790449.2790529.
  5. B. Demoen (1992): On the Transformation of a Prolog Program to a More Efficient Binary Program. In: K. Lau & T. Clement: Logic Program Synthesis and Transformation, Proceedings of LOPSTR 92, International Workshop on Logic Program Synthesis and Transformation, University of Manchester, UK, 2-3 July 1992, Workshops in Computing. Springer, pp. 242–252, doi:10.1007/978-1-4471-3560-9_17.
  6. T. Despeyroux (1984): Executable Specification of Static Semantics. In: G. Kahn, D. B. MacQueen & G. Plotkin: Semantics of Data Types, LNCS 173. Springer-Verlag, pp. 215233, doi:10.1007/3-540-13346-1_11.
  7. V. Donzeau-Gouge, G. Huet, G. Kahn & B. Lang (1984): Programming Environments Based on Structured Editors: The MENTOR experience. In: D. Barstow, E. Sandewall & H. Shrobe: Interactive Programming Environments * . McGraw-Hill, pp. 128140.
  8. Y. Futamura (1971): Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler. Systems, Computers, Controls 2(5), pp. 45–50.
  9. J. P. Gallagher, M. Hermenegildo, B. Kafle, M. Klemen, P. L. García & J. Morales (2020): Interpreters Repository. http://webhotel4.ruc.dk/~jpg/Software/Semantics.
  10. G. Gange, J. A. Navas, P. Schachte, H. Søndergaard & P. J. Stuckey (2015): Horn clauses as an intermediate representation for program analysis and transformation. Theory Pract. Log. Program. 15(4-5), pp. 526–542, doi:10.1017/S1471068415000204.
  11. M. Gómez-Zamalloa, E. Albert & G. Puebla (2009): Decompilation of Java bytecode to Prolog by partial evaluation. Inf. Softw. Technol. 51(10), pp. 1409–1427, doi:10.1016/j.infsof.2009.04.010.
  12. 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.
  13. A. Gurfinkel, T. Kahsai, A. Komuravelli & J. A. Navas (2015): The SeaHorn Verification Framework. In: D. Kroening & C. S. Pasareanu: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science 9206. Springer, pp. 343–361, doi:10.1007/978-3-319-21690-4_20.
  14. K. S. Henriksen & J. P. Gallagher (2006): Abstract Interpretation of PIC Programs through Logic Programming. In: Sixth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2006), 27-29 September 2006, Philadelphia, Pennsylvania, USA. IEEE Computer Society, pp. 184–196, doi:10.1109/SCAM.2006.1.
  15. M. V. Hermenegildo, F. Bueno, M. Carro, P. López-García, R. Haemmerlé, E. Mera, J. F. Morales & G. Puebla (2011): An Overview of the Ciao System. In: N. Bassiliades, G. Governatori & A. Paschke: Rule-Based Reasoning, Programming, and Applications - 5th International Symposium, RuleML 2011 - Europe, Barcelona, Spain, July 19-21, 2011. Proceedings, Lecture Notes in Computer Science 6826. Springer, pp. 2, doi:10.1007/978-3-642-22546-8_2.
  16. M. V. Hermenegildo, G. Puebla, F. Bueno & P. López-García (2005): Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor). Science of Computer Programming 58(1–2), doi:10.1016/j.scico.2005.02.006.
  17. C. A. R. Hoare (1969): An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), pp. 576–580, doi:10.1145/363235.363259.
  18. H. Hojjat & P. Rümmer (2018): The ELDARICA Horn Solver. In: N. Bjørner & A. Gurfinkel: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE, pp. 1–7, doi:10.23919/FMCAD.2018.8603013.
  19. B. Kafle & J. P. Gallagher (2017): Constraint specialisation in Horn clause verification. Sci. Comput. Program. 137, pp. 125–140, doi:10.1016/j.scico.2017.01.002.
  20. 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.
  21. B. Kafle, J. P. Gallagher & J. F. Morales (2016): RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pp. 261–268, doi:10.1007/978-3-319-41528-4_14.
  22. G. Kahn (1987): Natural Semantics. In: F. Brandenburg, G. Vidal-Naquet & M. Wirsing: STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, Lecture Notes in Computer Science 247. Springer, pp. 22–39, doi:10.1007/BFb0039592.
  23. T. Kahsai, P. Rümmer, H. Sanchez & M. Schäf (2016): JayHorn: A Framework for Verifying Java programs. In: S. Chaudhuri & A. Farzan: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science 9779. Springer, pp. 352–358, doi:10.1007/978-3-319-41528-4_19.
  24. Z. Kincaid, J. Breck, A. F. Boroujeni & T. W. Reps (2017): Compositional recurrence analysis revisited. In: A. Cohen & M. T. Vechev: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. ACM, pp. 248–262, doi:10.1145/3062341.3062373.
  25. M. Leuschel & J. Jørgensen (1999): Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN. Elec. Notes Theor. Comp. Sci. 30(2), doi:10.1017/S1471068403001662.
  26. M. Leuschel, D. Elphick, M. Varea, S. Craig & M. Fontaine (2006): The Ecce and Logen partial evaluators and their web interfaces. In: J. Hatcliff & F. Tip: PEPM. ACM, pp. 88–94, doi:10.1145/1111542.1111557.
  27. M. Leuschel & M. H. Sørensen (1996): Redundant Argument Filtering of Logic Programs. In: J. P. Gallagher: Logic Programming Synthesis and Transformation, 6th International Workshop, LOPSTR'96, Stockholm, Sweden, August 28-30, 1996, Proceedings, pp. 83–103, doi:10.1007/3-540-62718-9_6.
  28. J. Lloyd (1987): Foundations of Logic Programming: 2nd Edition. Springer-Verlag, doi:10.1007/978-3-642-83189-8.
  29. P. López-García, M. Klemen, U. Liqat & M. V. Hermenegildo (2016): A general framework for static profiling of parametric resource usage. Theory Pract. Log. Program. 16(5-6), pp. 849–865, doi:10.1017/S1471068416000442.
  30. K. Marriott, L. Naish & J. Lassez (1990): Most Specific Logic Programs. Ann. Math. Artif. Intell. 1, pp. 303–338, doi:10.1007/BF01531082.
  31. M. Méndez-Lojo, J. A. Navas & M. V. Hermenegildo (2007): A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In: A. King: Logic-Based Program Synthesis and Transformation, 17th International Symposium, LOPSTR 2007, Kongens Lyngby, Denmark, August 23-24, 2007, Revised Selected Papers, Lecture Notes in Computer Science 4915. Springer, pp. 154–168, doi:10.1007/978-3-540-78769-3_11.
  32. H. R. Nielson & F. Nielson (1992): Semantics with applications - a formal introduction. Wiley professional computing. Wiley.
  33. J. Peralta, J. P. Gallagher & H. Sağlam (1998): Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In: G. Levi: Static Analysis. 5th International Symposium, SAS'98, Pisa, Springer-Verlag Lecture Notes in Computer Science 1503, pp. 246–261, doi:10.1007/3-540-49727-7_15.
  34. 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.
  35. G. D. Plotkin (1981): A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.
  36. G. D. Plotkin (2004): The origins of structural operational semantics. J. Log. Algebr. Program. 60-61, pp. 3–15, doi:10.1016/j.jlap.2004.03.009.
  37. G. D. Plotkin (2004): A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, pp. 17–139, doi:10.1016/j.jlap.2004.03.009.
  38. R. E. Tarjan (1981): Fast Algorithms for Solving Path Problems. J. ACM 28(3), pp. 594–614, doi:10.1145/322261.322273.
  39. T. Wei, J. Mao, W. Zou & Y. Chen (2007): A New Algorithm for Identifying Loops in Decompilation. In: H. R. Nielson & G. Filé: Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Lecture Notes in Computer Science 4634. Springer, pp. 170–183, doi:10.1007/978-3-540-74061-2_11.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org