@inproceedings(DBLP:conf/birthday/BjornerGMR15, author = {Bj{\o}rner, N. and A. Gurfinkel and K. L. McMillan and A. Rybalchenko}, year = {2015}, title = {Horn Clause Solvers for Program Verification}, editor = {L. D. Beklemishev and A. Blass and N. Dershowitz and B. Finkbeiner and W. Schulte}, booktitle = {Fields of Logic and Computation {II}}, series = {LNCS}, volume = {9300}, publisher = {Springer}, pages = {24--51}, doi = {10.1007/978-3-319-23534-9\_2}, ) @article(BlazyL09, author = {S. Blazy and X. Leroy}, year = {2009}, title = {Mechanized Semantics for the Clight Subset of the {C} Language}, journal = {J. Autom. Reasoning}, volume = {43}, number = {3}, pages = {263--288}, doi = {10.1007/s10817-009-9148-3}, ) @article(DBLP:journals/scp/AngelisFPP14, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2014}, title = {Program verification via iterated specialization}, journal = {Sci. Comput. Program.}, volume = {95}, pages = {149--175}, doi = {10.1016/j.scico.2014.05.017}, ) @inproceedings(AngelisFPP15, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2015}, title = {Semantics-based generation of verification conditions by program specialization}, editor = {M. Falaschi and E. Albert}, booktitle = {Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015}, publisher = {{ACM}}, pages = {91--102}, doi = {10.1145/2790449.2790529}, ) @inproceedings(Demoen92, author = {B. Demoen}, year = {1992}, title = {On the Transformation of a Prolog Program to a More Efficient Binary Program}, editor = {K. Lau and T. Clement}, booktitle = {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}, series = {Workshops in Computing}, publisher = {Springer}, pages = {242--252}, doi = {10.1007/978-1-4471-3560-9\_17}, ) @inproceedings(Despeyroux1984, author = {T. Despeyroux}, year = {1984}, title = {Executable Specification of Static Semantics}, editor = {G. Kahn and D. B. MacQueen and G. Plotkin}, booktitle = {Semantics of Data Types}, series = {LNCS}, volume = {173}, publisher = {Springer-Verlag}, pages = {215\IeC{\textendash}233}, doi = {10.1007/3-540-13346-1_11}, ) @incollection(mentor1984, author = {Donzeau-Gouge, V. and G. Huet and G. Kahn and B. Lang}, year = {1984}, title = {Programming Environments Based on Structured Editors: The MENTOR experience}, editor = {D. Barstow and E. Sandewall and H. Shrobe}, booktitle = {Interactive Programming Environments}, isbn = {ISBN=978-0070038851}, publisher = {McGraw-Hill}, pages = {128\IeC{\textendash}140}, ) @article(Futamura, author = {Y. Futamura}, year = {1971}, title = {Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler}, journal = {Systems, Computers, Controls}, volume = {2(5)}, pages = {45--50}, ) @misc(interpreters, author = {J. P. Gallagher and M. Hermenegildo and B. Kafle and M. Klemen and P. L. Garc\'ia and J. Morales}, year = {2020}, title = {Interpreters Repository}, howpublished = {\url{http://webhotel4.ruc.dk/~jpg/Software/Semantics}}, ) @article(GangeNSSS15, author = {G. Gange and J. A. Navas and P. Schachte and S{\o}ndergaard, H. and P. J. Stuckey}, year = {2015}, title = {Horn clauses as an intermediate representation for program analysis and transformation}, journal = {Theory Pract. Log. Program.}, volume = {15}, number = {4-5}, pages = {526--542}, doi = {10.1017/S1471068415000204}, ) @article(Gomez-ZamalloaAP09, author = {G{\'{o}}mez{-}Zamalloa, M. and E. Albert and G. Puebla}, year = {2009}, title = {Decompilation of {J}ava bytecode to {P}rolog by partial evaluation}, journal = {Inf. Softw. Technol.}, volume = {51}, number = {10}, pages = {1409--1427}, doi = {10.1016/j.infsof.2009.04.010}, ) @inproceedings(GrebenshchikovLPR12, author = {S. Grebenshchikov and N. P. Lopes and C. Popeea and A. Rybalchenko}, year = {2012}, title = {Synthesizing software verifiers from proof rules}, editor = {J. Vitek and H. Lin and F. Tip}, booktitle = {ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12}, publisher = {ACM}, pages = {405--416}, doi = {10.1145/2254064.2254112}, ) @inproceedings(GurfinkelKKN15, author = {A. Gurfinkel and T. Kahsai and A. Komuravelli and J. A. Navas}, year = {2015}, title = {The SeaHorn Verification Framework}, editor = {D. Kroening and C. S. Pasareanu}, booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {9206}, publisher = {Springer}, pages = {343--361}, doi = {10.1007/978-3-319-21690-4\_20}, ) @inproceedings(HenriksenG06, author = {K. S. Henriksen and J. P. Gallagher}, year = {2006}, title = {Abstract Interpretation of {PIC} Programs through Logic Programming}, booktitle = {Sixth {IEEE} International Workshop on Source Code Analysis and Manipulation {(SCAM} 2006), 27-29 September 2006, Philadelphia, Pennsylvania, {USA}}, publisher = {{IEEE} Computer Society}, pages = {184--196}, doi = {10.1109/SCAM.2006.1}, ) @inproceedings(HermenegildoBCLHMMP11, author = {M. V. Hermenegildo and F. Bueno and M. Carro and L{\'{o}}pez{-}Garc{\'{\i}}a, P. and R. Haemmerl{\'{e}} and E. Mera and J. F. Morales and G. Puebla}, year = {2011}, title = {An Overview of the Ciao System}, editor = {N. Bassiliades and G. Governatori and A. Paschke}, booktitle = {Rule-Based Reasoning, Programming, and Applications - 5th International Symposium, RuleML 2011 - Europe, Barcelona, Spain, July 19-21, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6826}, publisher = {Springer}, pages = {2}, doi = {10.1007/978-3-642-22546-8\_2}, ) @article(ciaopp-sas03-journal-scp, author = {M. V. Hermenegildo and G. Puebla and F. Bueno and L\'{o}pez-Garc\'{\i}a, P.}, year = {2005}, title = {{I}ntegrated {P}rogram {D}ebugging, {V}erification, and {O}ptimization {U}sing {A}bstract {I}nterpretation (and {T}he {C}iao {S}ystem {P}reprocessor)}, journal = {Science of Computer Programming}, volume = {58}, number = {1--2}, doi = {10.1016/j.scico.2005.02.006}, ) @article(Hoare69, author = {C. A. R. Hoare}, year = {1969}, title = {An Axiomatic Basis for Computer Programming}, journal = {Commun. {ACM}}, volume = {12}, number = {10}, pages = {576--580}, doi = {10.1145/363235.363259}, ) @inproceedings(DBLP:conf/fmcad/HojjatR18, author = {H. Hojjat and P. R{\"{u}}mmer}, year = {2018}, title = {The {ELDARICA} {Horn} Solver}, editor = {Bj{\o}rner, N. and A. Gurfinkel}, booktitle = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin, TX, USA, October 30 - November 2, 2018}, publisher = {{IEEE}}, pages = {1--7}, doi = {10.23919/FMCAD.2018.8603013}, ) @article(KafleG17, author = {B. Kafle and J. P. Gallagher}, year = {2017}, title = {Constraint specialisation in Horn clause verification}, journal = {Sci. Comput. Program.}, volume = {137}, pages = {125--140}, doi = {10.1016/j.scico.2017.01.002}, ) @article(DBLP:journals/tplp/KafleGG18, author = {B. Kafle and J. P. Gallagher and P. Ganty}, year = {2018}, title = {Tree dimension in verification of constrained Horn clauses}, journal = {{TPLP}}, volume = {18}, number = {2}, pages = {224--251}, doi = {10.1017/S1471068418000030}, ) @inproceedings(DBLP:conf/cav/KafleGM16, author = {B. Kafle and J. P. Gallagher and J. F. Morales}, year = {2016}, title = {{RAHFT}: {A} Tool for Verifying {H}orn Clauses Using Abstract Interpretation and Finite Tree Automata}, booktitle = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}}, pages = {261--268}, doi = {10.1007/978-3-319-41528-4_14}, ) @inproceedings(Kahn87, author = {G. Kahn}, year = {1987}, title = {Natural Semantics}, editor = {F. Brandenburg and Vidal{-}Naquet, G. and M. Wirsing}, booktitle = {{STACS} 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {247}, publisher = {Springer}, pages = {22--39}, doi = {10.1007/BFb0039592}, ) @inproceedings(KahsaiRSS16, author = {T. Kahsai and P. R{\"{u}}mmer and H. Sanchez and M. Sch{\"{a}}f}, year = {2016}, title = {JayHorn: {A} Framework for Verifying Java programs}, editor = {S. Chaudhuri and A. Farzan}, booktitle = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {9779}, publisher = {Springer}, pages = {352--358}, doi = {10.1007/978-3-319-41528-4\_19}, ) @inproceedings(KincaidBBR17, author = {Z. Kincaid and J. Breck and A. F. Boroujeni and T. W. Reps}, year = {2017}, title = {Compositional recurrence analysis revisited}, editor = {A. Cohen and M. T. Vechev}, booktitle = {Proceedings of the 38th {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2017, Barcelona, Spain, June 18-23, 2017}, publisher = {{ACM}}, pages = {248--262}, doi = {10.1145/3062341.3062373}, ) @article(Logen, author = {M. Leuschel and J{\o}rgensen, J.}, year = {1999}, title = {Efficient Specialisation in {P}rolog Using the Hand-Written Compiler Generator {LOGEN}}, journal = {Elec. Notes Theor. Comp. Sci.}, volume = {30(2)}, doi = {10.1017/S1471068403001662}, ) @inproceedings(LeuschelEVCF06, author = {M. Leuschel and D. Elphick and M. Varea and S. Craig and M. Fontaine}, year = {2006}, title = {The {Ecce} and {Logen} partial evaluators and their web interfaces}, editor = {J. Hatcliff and F. Tip}, booktitle = {PEPM}, publisher = {{ACM}}, pages = {88--94}, doi = {10.1145/1111542.1111557}, ) @inproceedings(LeuschelS96a, author = {M. Leuschel and S{\o}rensen, M. H.}, year = {1996}, title = {Redundant Argument Filtering of Logic Programs}, editor = {J. P. Gallagher}, booktitle = {Logic Programming Synthesis and Transformation, 6th International Workshop, LOPSTR'96, Stockholm, Sweden, August 28-30, 1996, Proceedings}, pages = {83--103}, doi = {10.1007/3-540-62718-9\_6}, ) @book(Lloyd, author = {J. Lloyd}, year = {1987}, title = {Foundations of Logic Programming: 2nd Edition}, publisher = {Springer-Verlag}, doi = {10.1007/978-3-642-83189-8}, ) @article(Lopez-GarciaKLH16, author = {L{\'{o}}pez{-}Garc{\'{\i}}a, P. and M. Klemen and U. Liqat and M. V. Hermenegildo}, year = {2016}, title = {A general framework for static profiling of parametric resource usage}, journal = {Theory Pract. Log. Program.}, volume = {16}, number = {5-6}, pages = {849--865}, doi = {10.1017/S1471068416000442}, ) @article(MarriottNL90, author = {K. Marriott and L. Naish and J. Lassez}, year = {1990}, title = {Most Specific Logic Programs}, journal = {Ann. Math. Artif. Intell.}, volume = {1}, pages = {303--338}, doi = {10.1007/BF01531082}, ) @inproceedings(Mendez-LojoNH07, author = {M{\'{e}}ndez{-}Lojo, M. and J. A. Navas and M. V. Hermenegildo}, year = {2007}, title = {A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs}, editor = {A. King}, booktitle = {Logic-Based Program Synthesis and Transformation, 17th International Symposium, {LOPSTR} 2007, Kongens Lyngby, Denmark, August 23-24, 2007, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {4915}, publisher = {Springer}, pages = {154--168}, doi = {10.1007/978-3-540-78769-3\_11}, ) @book(NielsonN1992, author = {H. R. Nielson and F. Nielson}, year = {1992}, title = {Semantics with applications - a formal introduction}, series = {Wiley professional computing}, publisher = {Wiley}, ) @inproceedings(Peralta-Gallagher-Saglam-SAS98, author = {J. Peralta and J. P. Gallagher and Sa\u{g}lam, H.}, year = {1998}, title = {Analysis of Imperative Programs through Analysis of Constraint Logic Programs}, editor = {G. Levi}, booktitle = {Static Analysis. 5th International Symposium, SAS'98, Pisa}, series = {Springer-Verlag Lecture Notes in Computer Science}, volume = {1503}, pages = {246--261}, doi = {10.1007/3-540-49727-7\_15}, ) @article(Pettorossi-Proietti, author = {A. Pettorossi and M. Proietti}, year = {1999}, title = {Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs.}, journal = {J. Log. Program.}, volume = {41}, number = {2-3}, pages = {197--230}, doi = {10.1016/S0743-1066(99)00029-1}, ) @techreport(Plotkin1981, author = {G. D. Plotkin}, year = {1981}, title = {A Structural Approach to Operational Semantics}, type = {Technical Report}, number = {DAIMI FN-19}, institution = {Computer Science Department, Aarhus University}, ) @article(Plotkin04, author = {G. D. Plotkin}, year = {2004}, title = {The origins of structural operational semantics}, journal = {J. Log. Algebr. Program.}, volume = {60-61}, pages = {3--15}, doi = {10.1016/j.jlap.2004.03.009}, ) @article(Plotkin04a, author = {G. D. Plotkin}, year = {2004}, title = {A structural approach to operational semantics}, journal = {J. Log. Algebr. Program.}, volume = {60-61}, pages = {17--139}, doi = {10.1016/j.jlap.2004.03.009}, ) @article(Tarjan81b, author = {R. E. Tarjan}, year = {1981}, title = {Fast Algorithms for Solving Path Problems}, journal = {J. {ACM}}, volume = {28}, number = {3}, pages = {594--614}, doi = {10.1145/322261.322273}, ) @inproceedings(WeiMZC07, author = {T. Wei and J. Mao and W. Zou and Y. Chen}, year = {2007}, title = {A New Algorithm for Identifying Loops in Decompilation}, editor = {H. R. Nielson and G. Fil{\'{e}}}, booktitle = {Static Analysis, 14th International Symposium, {SAS} 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4634}, publisher = {Springer}, pages = {170--183}, doi = {10.1007/978-3-540-74061-2\_11}, )