References

  1. Mathematica: the Way the World Calculates. http://www.wolfram.com/products/mathematica/index.html.
  2. Elvira Albert, Samir Genaim & Abu Naser Masud (2013): On the Inference of Resource Usage Upper and Lower Bounds. ACM Trans. Comput. Log. 14(3), pp. 22:1–22:35. Available at https://doi.org/10.1145/2499937.2499943.
  3. R. Bagnara, F. Mesnard, A. Pescetti & E. Zaffanella (2010): The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version. Quaderno 498. Dipartimento di Matematica, Università di Parma, Italy. Available at http://www.cs.unipr.it/Publications/.
  4. Rod M. Burstall & John Darlington (1977): A transformation system for developing recursive programs. Journal of the ACM 24(1), pp. 44–67. Available at https://doi.org/10.1145/356635.356640.
  5. John Cyphert, Jason Breck, Zachary Kincaid & Thomas W. Reps (2019): Refinement of path expressions for static analysis = "POPL",, pp. 45:1–45:29. Available at https://doi.org/10.1145/3290358.
  6. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2015): Semantics-based generation of verification conditions by program specialization. In: PPDP. ACM, pp. 91–102. Available at https://doi.org/10.1145/2790449.2790529.
  7. S. K. Debray & N. W. Lin (1993): Cost Analysis of Logic Programs. ACM Transactions on Programming Languages and Systems 15(5), pp. 826–875. Available at https://doi.org/10.1145/361002.361016.
  8. S. K. Debray, N.-W. Lin & M. V. Hermenegildo (1990): Task Granularity Analysis in Logic Programs. In: PLDI. ACM Press, pp. 174–188. Available at https://doi.org/10.1145/93548.93564.
  9. Saumya K. Debray & Nai-Wei Lin (1993): Cost Analysis of Logic Programs. ACM Trans. Program. Lang. Syst. 15(5), pp. 826–875. Available at https://doi.org/10.1145/161468.161472.
  10. Jesús J. Doménech, John P. Gallagher & Samir Genaim (2019): Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. TPLP 19(5-6), pp. 990–1005. Available at https://doi.org/10.1017/S1471068419000310.
  11. Azadeh Farzan & Zachary Kincaid (2015): Compositional Recurrence Analysis. In: Roope Kaivola & Thomas Wahl: FMCAD. IEEE, pp. 57–64. Available at https://doi.org/10.5555/2893529.2893544.
  12. J. Gallagher, M. V. Hermenegildo, B. Kafle, M. Klemen, P. Lopez-Garcia & J.F. Morales (2020): From big-step to small-step semantics and back with interpreter specialization (invited paper). In: VPT, EPTCS. Open Publishing Association, pp. 50–65. Available at https://doi.org/10.4204/EPTCS.320.4.
  13. M. Gómez-Zamalloa, E. Albert & G. Puebla (2009): Decompilation of Java Bytecode to Prolog by Partial Evaluation. JIST 51, pp. 1409–1427. Available at https://doi.org/10.1016/j.infsof.2009.04.010.
  14. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: Jan Vitek, Haibo Lin & Frank Tip: PLDI. ACM, pp. 405–416. Available at https://doi.org/10.1145/2254064.2254112.
  15. Sumit Gulwani, Sagar Jain & Eric Koskinen (2009): Control-flow refinement and progress invariants for bound analysis. In: Michael Hind & Amer Diwan: PLDI. ACM, pp. 375–385. Available at https://doi.org/10.1145/1543135.1542518.
  16. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli & Jorge A. Navas (2015): The SeaHorn Verification Framework. In: CAV, LNCS 9206. Springer, pp. 343–361. Available at https://doi.org/10.1007/978-3-319-21690-4_20.
  17. Kim S. Henriksen & John P. Gallagher (2006): Abstract Interpretation of PIC Programs through Logic Programming. In: SCAM '06. IEEE Computer Society, pp. 184–196. Available at https://doi.org/10.1109/SCAM.2006.1.
  18. M. Hermenegildo, G. Puebla, F. Bueno & P. Lopez Garcia (2005): Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor). Science of Computer Programming 58(1–2), pp. 115–140. Available at https://doi.org/10.1016/j.scico.2005.02.006.
  19. Andreas Humenberger, Maximilian Jaroschek & Laura Kovács (2018): Invariant Generation for Multi-Path Loops with Polynomial Assignments. In: Isil Dillig & Jens Palsberg: VMCAI, LNCS 10747. Springer, pp. 226–246. Available at https://doi.org/10.1007/978-3-319-73721-8_11.
  20. Bishoksan Kafle, John P. Gallagher & Pierre Ganty (2016): Solving non-linear Horn clauses using a linear Horn clause solver. In: John P. Gallagher & Philipp Rümmer: HCVS, EPTCS 219, pp. 33–48. Available at https://doi.org/10.4204/EPTCS.219.4.
  21. Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez & Martin Schäf (2016): JayHorn: A Framework for Verifying Java Programs. In: Swarat Chaudhuri & Azadeh Farzan: CAV, LNCS 9779. Springer, pp. 352–358. Available at https://doi.org/10.1007/978-3-319-41528-4_19.
  22. Zachary Kincaid, Jason Breck, John Cyphert & Thomas W. Reps (2019): Closed forms for numerical loops. Proc. ACM Program. Lang. 3(POPL), pp. 55:1–55:29. Available at https://doi.org/10.1145/3290368.
  23. Zachary Kincaid, John Cyphert, Jason Breck & Thomas W. Reps (2018): Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), pp. 54:1–54:33. Available at https://doi.org/10.1145/3158142.
  24. M. Méndez-Lojo, J. Navas & M. Hermenegildo (2007): A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In: LOPSTR, LNCS 4915. Springer-Verlag, pp. 154–168. Available at https://doi.org/10.1007/978-3-540-78769-3_11.
  25. K. Muthukumar & M. Hermenegildo (1990): Deriving A Fixpoint Computation Algorithm for Top-down Abstract Interpretation of Logic Programs. Technical Report ACT-DC-153-90. Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759. Available at ftp://cliplab.org/pub/papers/tr153-90.mcc.ps.Z.
  26. J. Navas, E. Mera, P. Lopez-Garcia & M. Hermenegildo (2007): User-Definable Resource Bounds Analysis for Logic Programs. In: ICLP, LNCS 4670. Springer, pp. 348–363. Available at https://doi.org/10.1007/978-3-540-74610-2_24. 10-year Test of Time Award.
  27. Flemming Nielson, Hanne Riis Nielson & Chris Hankin (1999): Principles of program analysis. Springer. Available at https://doi.org/10.1007/978-3-662-03811-6.
  28. J.C. Peralta, J. Gallagher & H. Sağlam (1998): Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In: G. Levi: SAS, LNCS 1503, pp. 246–261. Available at https://doi.org/10.1007/3-540-49727-7_15.
  29. A. Podelski & A. Rybalchenko (2004): A Complete Method for the Synthesis of Linear Ranking Functions. In: VMCAI, LNCS. Springer, pp. 239–251. Available at https://doi.org/10.1007/978-3-540-24622-0_20.
  30. G. Puebla & M. V. Hermenegildo (1999): Abstract Multiple Specialization and its Application to Program Parallelization. J. of Logic Programming. Special Issue on Synthesis, Transformation and Analysis of Logic Programs 41(2&3), pp. 279–316. Available at https://doi.org/10.1016/S0743-1066(99)00031-X.
  31. Rahul Sharma, Isil Dillig, Thomas Dillig & Alex Aiken (2011): Simplifying Loop Invariant Generation Using Splitter Predicates. In: Ganesh Gopalakrishnan & Shaz Qadeer: CAV, LNCS 6806. Springer, pp. 703–719. Available at https://doi.org/10.1007/978-3-642-22110-1_57.
  32. Kirack Sohn & Allen Van Gelder (1991): Termination detection in logic programs using argument sizes (extended abstract). In: PODS. ACM Press, New York, NY, USA, pp. 216–226. Available at https://doi.org/10.1145/113413.113433.
  33. Robert E. Tarjan (1981): Fast Algorithms for Solving Path Problems. J. ACM 28(3), pp. 594–614. Available at https://doi.org/10.1145/322261.322273.
  34. B. Wegbreit (1974): The Treatment of Data Types in EL1. Comm. of the ACM 17(5), pp. 251–264. Available at https://doi.org/10.1145/364063.364092.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org