@misc(mathematica, title = {Mathematica: the {W}ay the {W}orld {C}alculates}, note = {\newline\texttt {http://www.wolfram.com/products/mathematica/index.html}}, ) @article(AlbertGM13, author = {Elvira Albert and Samir Genaim and Abu Naser Masud}, year = {2013}, title = {On the Inference of Resource Usage Upper and Lower Bounds}, journal = {{ACM} Trans. Comput. Log.}, volume = {14}, number = {3}, pages = {22:1--22:35}, url = {https://doi.org/10.1145/2499937.2499943}, ) @techreport(BagnaraMPZ10TR, author = {R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella}, year = {2010}, title = {The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version}, type = {Quaderno}, number = {498}, institution = {Dipartimento di Matematica, Universit\`a di Parma, Italy}, note = {Available at \url{http://www.cs.unipr.it/Publications/}}, ) @article(Burstall:77:78, author = {Rod M. Burstall and John Darlington}, year = {1977}, title = {A transformation system for developing recursive programs}, journal = {Journal of the ACM}, volume = {24}, number = {1}, pages = {44--67}, url = {https://doi.org/10.1145/356635.356640}, ) @article(Cyphertpopl19, author = {John Cyphert and Jason Breck and Zachary Kincaid and Thomas W. Reps}, year = {2019}, title = {Refinement of path expressions for static analysis}, = "{POPL}", pages = {45:1--45:29}, url = {https://doi.org/10.1145/3290358}, ) @inproceedings(AngelisFPP15-short, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2015}, title = {Semantics-based generation of verification conditions by program specialization}, booktitle = {{PPDP}}, publisher = {{ACM}}, pages = {91--102}, url = {https://doi.org/10.1145/2790449.2790529}, ) @article(caslog, author = {S. K. Debray and N. W. Lin}, year = {1993}, title = {{Cost Analysis of Logic Programs}}, journal = {{ACM} Transactions on Programming Languages and Systems}, volume = {15}, number = {5}, pages = {826--875}, url = {https://doi.org/10.1145/361002.361016}, ) @inproceedings(granularity, author = {S. K. Debray and N.-W. Lin and M. V. Hermenegildo}, year = {1990}, title = {{T}ask {G}ranularity {A}nalysis in {L}ogic {P}rograms}, booktitle = {{PLDI}}, publisher = {{ACM} Press}, pages = {174--188}, url = {https://doi.org/10.1145/93548.93564}, ) @article(DBLP:journals/toplas/DebrayL93, author = {Saumya K. Debray and Nai{-}Wei Lin}, year = {1993}, title = {Cost Analysis of Logic Programs}, journal = {{ACM} Trans. Program. Lang. Syst.}, volume = {15}, number = {5}, pages = {826--875}, url = {https://doi.org/10.1145/161468.161472}, ) @article(DomenechGG19, author = {Jes{\'{u}}s J. Dom{\'{e}}nech and John P. Gallagher and Samir Genaim}, year = {2019}, title = {Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis}, journal = {{TPLP}}, volume = {19}, number = {5-6}, pages = {990--1005}, url = {https://doi.org/10.1017/S1471068419000310}, ) @inproceedings(farzanfmcad15, author = {Azadeh Farzan and Zachary Kincaid}, year = {2015}, title = {Compositional Recurrence Analysis}, editor = {Roope Kaivola and Thomas Wahl}, booktitle = {{FMCAD}}, publisher = {{IEEE}}, pages = {57--64}, url = {https://doi.org/10.5555/2893529.2893544}, ) @inproceedings(big-small-step-vpt2020-short, author = {J. Gallagher and M. V. Hermenegildo and B. Kafle and M. Klemen and Lopez-Garcia, P. and J.F. Morales}, year = {2020}, title = {From big-step to small-step semantics and back with interpreter specialization (invited paper)}, booktitle = {{VPT}}, series = {EPTCS}, publisher = {Open Publishing Association}, pages = {50--65}, url = {https://doi.org/10.4204/EPTCS.320.4}, ) @article(mod-decomp-jist09-short, author = {G\'{o}mez-Zamalloa, M. and E. Albert and G. Puebla}, year = {2009}, title = {{D}ecompilation of {J}ava {B}ytecode to {P}rolog by {P}artial {E}valuation}, journal = {JIST}, volume = {51}, pages = {1409--1427}, url = {https://doi.org/10.1016/j.infsof.2009.04.010}, ) @inproceedings(GrebenshchikovLPR12, author = {Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko}, year = {2012}, title = {Synthesizing software verifiers from proof rules}, editor = {Jan Vitek and Haibo Lin and Frank Tip}, booktitle = {{PLDI}}, publisher = {ACM}, pages = {405--416}, url = {https://doi.org/10.1145/2254064.2254112}, ) @inproceedings(GulwaniJK09, author = {Sumit Gulwani and Sagar Jain and Eric Koskinen}, year = {2009}, title = {Control-flow refinement and progress invariants for bound analysis}, editor = {Michael Hind and Amer Diwan}, booktitle = {{PLDI}}, publisher = {{ACM}}, pages = {375--385}, url = {https://doi.org/10.1145/1543135.1542518}, ) @inproceedings(GurfinkelKKN15-short, author = {Arie Gurfinkel and Temesghen Kahsai and Anvesh Komuravelli and Jorge A. Navas}, year = {2015}, title = {{T}he {S}ea{H}orn {V}erification {F}ramework}, booktitle = {{CAV}}, series = {LNCS}, volume = {9206}, publisher = {Springer}, pages = {343--361}, url = {https://doi.org/10.1007/978-3-319-21690-4_20}, ) @inproceedings(HGScam06-short, author = {Kim S. Henriksen and John P. Gallagher}, year = {2006}, title = {{A}bstract {I}nterpretation of {PIC} {P}rograms through {L}ogic {P}rogramming}, booktitle = {SCAM~'06}, publisher = {IEEE Computer Society}, pages = {184--196}, url = {https://doi.org/10.1109/SCAM.2006.1}, ) @article(ciaopp-sas03-journal-scp-short, author = {M. Hermenegildo and G. Puebla and F. Bueno and P. Lopez Garcia}, 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}, pages = {115--140}, url = {https://doi.org/10.1016/j.scico.2005.02.006}, ) @inproceedings(Humenbergervmcai18, author = {Andreas Humenberger and Maximilian Jaroschek and Laura Kov{\'{a}}cs}, year = {2018}, title = {Invariant Generation for Multi-Path Loops with Polynomial Assignments}, editor = {Isil Dillig and Jens Palsberg}, booktitle = {{VMCAI}}, series = {LNCS}, volume = {10747}, publisher = {Springer}, pages = {226--246}, url = {https://doi.org/10.1007/978-3-319-73721-8\_11}, ) @inproceedings(Kaflehcvs16, author = {Bishoksan Kafle and John P. Gallagher and Pierre Ganty}, year = {2016}, title = {Solving non-linear Horn clauses using a linear Horn clause solver}, editor = {John P. Gallagher and Philipp R{\"{u}}mmer}, booktitle = {{HCVS}}, series = {{EPTCS}}, volume = {219}, pages = {33--48}, url = {https://doi.org/10.4204/EPTCS.219.4}, ) @inproceedings(KahsaiRSS16-short, author = {Temesghen Kahsai and Philipp R{\"{u}}mmer and Huascar Sanchez and Martin Sch{\"{a}}f}, year = {2016}, title = {{JayHorn}: {A} Framework for Verifying {J}ava Programs}, editor = {Swarat Chaudhuri and Azadeh Farzan}, booktitle = {{CAV}}, series = {LNCS}, volume = {9779}, publisher = {Springer}, pages = {352--358}, url = {https://doi.org/10.1007/978-3-319-41528-4\_19}, ) @article(kincaidpopl19, author = {Zachary Kincaid and Jason Breck and John Cyphert and Thomas W. Reps}, year = {2019}, title = {Closed forms for numerical loops}, journal = {Proc. {ACM} Program. Lang.}, volume = {3}, number = {{POPL}}, pages = {55:1--55:29}, url = {https://doi.org/10.1145/3290368}, ) @article(kincaidpopl18, author = {Zachary Kincaid and John Cyphert and Jason Breck and Thomas W. Reps}, year = {2018}, title = {Non-linear reasoning for invariant synthesis}, journal = {Proc. {ACM} Program. Lang.}, volume = {2}, number = {{POPL}}, pages = {54:1--54:33}, url = {https://doi.org/10.1145/3158142}, ) @inproceedings(decomp-oo-prolog-lopstr07-short, author = {M\'{e}ndez-Lojo, M. and J. Navas and M. Hermenegildo}, year = {2007}, title = {{A} {F}lexible ({C}){LP}-{B}ased {A}pproach to the {A}nalysis of {O}bject-{O}riented {P}rograms}, booktitle = {LOPSTR}, series = {LNCS}, volume = {4915}, publisher = {Springer-Verlag}, pages = {154--168}, url = {https://doi.org/10.1007/978-3-540-78769-3_11}, ) @techreport(mcctr-fixpt, author = {K. Muthukumar and M. Hermenegildo}, year = {1990}, title = {{D}eriving {A} {F}ixpoint {C}omputation {A}lgorithm for {T}op-down {A}bstract {I}nterpretation of {L}ogic {P}rograms}, type = {Technical Report}, number = {ACT-DC-153-90}, institution = {Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759}, url = {ftp://cliplab.org/pub/papers/tr153-90.mcc.ps.Z}, ) @inproceedings(resource-iclp07, author = {J. Navas and E. Mera and Lopez-Garcia, P. and M. Hermenegildo}, year = {2007}, title = {{U}ser-{D}efinable {R}esource {B}ounds {A}nalysis for {L}ogic {P}rograms}, booktitle = {{ICLP}}, series = {LNCS}, volume = {4670}, publisher = {Springer}, pages = {348--363}, url = {https://doi.org/10.1007/978-3-540-74610-2_24}, note = {10-year Test of Time Award}, ) @book(popa-nielson, author = {Flemming Nielson and Hanne Riis Nielson and Chris Hankin}, year = {1999}, title = {Principles of program analysis}, publisher = {Springer}, url = {https://doi.org/10.1007/978-3-662-03811-6}, ) @inproceedings(Peralta-Gallagher-Saglam-SAS98, author = {J.C. Peralta and J. Gallagher and Sa\u{g}lam, H.}, year = {1998}, title = {Analysis of Imperative Programs through Analysis of Constraint Logic Programs}, editor = {G. Levi}, booktitle = {{SAS}}, series = {LNCS}, volume = {1503}, pages = {246--261}, url = {https://doi.org/10.1007/3-540-49727-7_15}, ) @inproceedings(PodelskiR04b, author = {A. Podelski and A. Rybalchenko}, year = {2004}, title = {A {C}omplete {M}ethod for the {S}ynthesis of {L}inear {R}anking {F}unctions}, booktitle = {{VMCAI}}, series = {LNCS}, publisher = {Springer}, pages = {239--251}, url = {https://doi.org/10.1007/978-3-540-24622-0_20}, ) @article(spec-jlp, author = {G. Puebla and M. V. Hermenegildo}, year = {1999}, title = {{A}bstract {M}ultiple {S}pecialization and its {A}pplication to {P}rogram {P}arallelization}, journal = {J.~of Logic Programming. Special Issue on Synthesis, Transformation and Analysis of Logic Programs}, volume = {41}, number = {2\&3}, pages = {279--316}, url = {https://doi.org/10.1016/S0743-1066(99)00031-X}, ) @inproceedings(Sharmacav11, author = {Rahul Sharma and Isil Dillig and Thomas Dillig and Alex Aiken}, year = {2011}, title = {Simplifying Loop Invariant Generation Using Splitter Predicates}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, booktitle = {{CAV}}, series = {LNCS}, volume = {6806}, publisher = {Springer}, pages = {703--719}, url = {https://doi.org/10.1007/978-3-642-22110-1\_57}, ) @inproceedings(113433, author = {Kirack Sohn and Allen Van Gelder}, year = {1991}, title = {Termination detection in logic programs using argument sizes (extended abstract)}, booktitle = {{PODS}}, publisher = {ACM Press}, address = {New York, NY, USA}, pages = {216--226}, url = {https://doi.org/10.1145/113413.113433}, ) @article(tarjan81, author = {Robert E. Tarjan}, year = {1981}, title = {Fast Algorithms for Solving Path Problems}, journal = {J. ACM}, volume = {28}, number = {3}, pages = {594--614}, url = {https://doi.org/10.1145/322261.322273}, ) @article(Wegbreit74, author = {B. Wegbreit}, year = {1974}, title = {The Treatment of Data Types in EL1}, journal = {Comm. of the ACM}, volume = {17}, number = {5}, pages = {251--264}, url = {https://doi.org/10.1145/364063.364092}, )