@incollection(Al&07, author = {E. Albert and G\'{o}mez-Zamalloa, M. and L. Hubert and G. Puebla}, year = {2007}, title = {Verification of {J}ava {B}ytecode {U}sing {A}nalysis and {T}ransformation of {L}ogic {P}rograms}, editor = {M. Hanus}, booktitle = {Practical {A}spects of {D}eclarative {L}anguages}, series = {Lecture Notes in Computer Science 4354}, publisher = {Springer}, pages = {124--139}, doi = {10.1007/978-3-540-69611-7\_8}, ) @book(Ap&09, author = {K. R. Apt and {de Boer}, F. S. and E.-R. Olderog}, year = {2009}, title = {Verification of Sequential and Concurrent Programs}, edition = {{T}hird}, publisher = {Springer}, doi = {10.1007/978-1-84882-745-5}, ) @inproceedings(BaG08, author = {G. Banda and J. P. Gallagher}, year = {2009}, title = {Analysis of Linear Hybrid Systems in {CLP}}, editor = {Michael Hanus}, booktitle = {Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17--18, 2008, Revised Selected Papers}, series = {Lecture Notes in Computer Science 5438}, publisher = {Springer}, pages = {55--70}, doi = {10.1007/978-3-642-00515-2\_5}, ) @inproceedings(Bj&15, 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} - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday}, series = {Lecture Notes in Computer Science 9300}, publisher = {Springer}, pages = {24--51}, doi = {10.1007/978-3-319-23534-9\_2}, ) @article(BruynoogheCGGV07, author = {M. Bruynooghe and M. Codish and J. P. Gallagher and S. Genaim and W. Vanhoof}, year = {2007}, title = {Termination analysis of logic programs through combination of type-based norms}, journal = {{ACM} Trans. Program. Lang. Syst.}, volume = {29}, number = {2}, pages = {10--es}, doi = {10.1145/1216374.1216378}, ) @incollection(Bun01, author = {A. Bundy}, year = {2001}, title = {The Automation of Proof by Mathematical Induction}, editor = {A. Robinson and A. Voronkov}, booktitle = {Handbook of Automated Reasoning}, volume = {I}, publisher = {North Holland}, pages = {845--911}, doi = {10.1016/B978-044450813-3/50015-1}, ) @article(BuD77, author = {R. M. Burstall and J. Darlington}, year = {1977}, title = {A Trans\-form\-ation System for Developing Recursive Pro\-grams}, journal = {Journal of the {ACM}}, volume = {24}, number = {1}, pages = {44--67}, doi = {10.1145/321992.321996}, ) @inproceedings(CertezeanuDELSW16, author = {R. Certezeanu and S. Drossopoulou and Egelund{-}M{\"{u}}ller, B. and K. R. M. Leino and S. Sivarajan and M. J. Wheelhouse}, year = {2016}, title = {Quicksort Revisited - {V}erifying Alternative Versions of Quicksort}, editor = {E. {\'{A}}brah{\'{a}}m and M. M. Bonsangue and E. Broch Johnsen}, booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science 9660}, publisher = {Springer}, pages = {407--426}, doi = {10.1007/978-3-319-30734-3\_27}, ) @article(De&14c, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2014}, title = {Program Verification via Iterated Specialization}, journal = {Science of Computer Programming}, volume = {95, Part 2}, pages = {149--175}, doi = {10.1016/j.scico.2014.05.017}, ) @inproceedings(De&14b, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2014}, title = {{V}eri{MAP}: {A} {T}ool for {V}erifying {P}rograms through {T}ransformations}, booktitle = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS~'14}, series = {Lecture Notes in Computer Science 8413}, publisher = {Springer}, pages = {568--574}, doi = {10.1007/978-3-642-54862-8\_47}, url = {http://www.map.uniroma2.it/VeriMAP}, ) @article(De&17b, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2017}, title = {Semantics-based generation of verification conditions via program specialization}, journal = {Science of Computer Programming}, volume = {147}, pages = {78--108}, doi = {10.1016/j.scico.2016.11.002}, ) @article(De&18a, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2018}, title = {Solving {H}orn Clauses on Inductive Data Types Without Induction}, journal = {Theory and Practice of Logic Programming}, volume = {18}, number = {3-4}, pages = {452--469}, doi = {10.1017/S1471068418000157}, note = {Special Issue on {\it ICLP~'18}}, ) @inproceedings(De&20a, author = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2020}, title = {Removing Algebraic Data Types from Constrained {H}orn Clauses Using Difference Predicates}, booktitle = {Proceedings of the International Joint Conference on Automated Reasoning, IJCAR~'20}, series = {Lecture Notes in Computer Science 12166}, publisher = {Springer, Cham}, pages = {83--102}, doi = {10.1007/978-3-030-51074-9_6}, ) @inproceedings(DeP99, author = {G. Delzanno and A. Podelski}, year = {1999}, title = {Model Checking in {CLP}}, editor = {R. Cleaveland}, booktitle = {5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,~TACAS~'99}, series = {Lecture Notes in Computer Science 1579}, publisher = {Springer-Verlag}, pages = {223--239}, doi = {10.1007/3-540-49059-0_16}, ) @article(EtG96, author = {S. Etalle and M. Gabbrielli}, year = {1996}, title = {Trans\-form\-ations of {CLP} Modules}, journal = {Theoretical Computer Science}, volume = {166}, pages = {101--146}, doi = {10.1016/0304-3975(95)00148-4}, ) @inproceedings(Fi&01a, author = {F. Fioravanti and A. Pettorossi and M. Proietti}, year = {2001}, title = {Verifying {CTL} Properties of Infinite State Systems by Specializing Constraint Logic Programs}, booktitle = {Proceedings of the {ACM SIGPLAN} Workshop on Verification and Computational Logic VCL'01, Florence (Italy)}, series = {Technical Report DSSE-TR-2001-3}, publisher = {University of Southampton, UK}, pages = {85--96}, ) @article(FoleyH71, author = {M. Foley and C. A. R. Hoare}, year = {1971}, title = {Proof of a Recursive Program: {Q}uicksort}, journal = {Comput. J.}, volume = {14}, number = {4}, pages = {391--395}, doi = {10.1093/comjnl/14.4.391}, ) @article(FrO97a, author = {L. Fribourg and H. Ols\'en}, year = {1997}, title = {A decompositional approach for computing least fixed-points of {D}atalog programs with {Z}-counters}, journal = {Constraints}, volume = {2}, number = {3/4}, pages = {305--335}, doi = {10.1023/A:1009747629591}, ) @inproceedings(Gr&12, author = {S. Grebenshchikov and N. P. Lopes and C. Popeea and A. Rybalchenko}, year = {2012}, title = {Synthesizing software verifiers from proof rules}, booktitle = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI~'12}, pages = {405--416}, doi = {10.1145/2345156.2254112}, ) @article(HamzaVK19, author = {J. Hamza and N. Voirol and V. Kuncak}, year = {2019}, title = {System {FR:} formalized foundations for the {S}tainless verifier}, journal = {Proc. {ACM} Program. Lang.}, volume = {3}, number = {{OOPSLA}}, pages = {166:1--166:30}, doi = {10.1145/3360592}, ) @article(Hoare61, author = {C. A. R. Hoare}, year = {1961}, title = {Algorithm 64: Quicksort}, journal = {Commun. {ACM}}, volume = {4}, number = {7}, pages = {321}, doi = {10.1145/366622.366644}, ) @article(Hoa69, author = {C.A.R. Hoare}, year = {1969}, title = {An {A}xiomatic {B}asis for {C}omputer {P}rogramming}, journal = {CACM}, volume = {12}, number = {10}, pages = {576--580, 583}, doi = {10.1145/363235.363259}, ) @article(Hog81, author = {C. J. Hogger}, year = {1981}, title = {Derivation of Logic Pro\-grams}, journal = {Journal of the {ACM}}, volume = {28}, number = {2}, pages = {372--392}, doi = {10.1145/322248.322258}, ) @inproceedings(HoR18, author = {H. Hojjat and Ph. R{\"{u}}mmer}, year = {2018}, title = {The {ELDARICA} {H}orn Solver}, editor = {Bj{\o}rner, N. and A. Gurfinkel}, booktitle = {2018 Formal Methods in Computer Aided Design, \unhbox\voidb@x \hbox{FMCAD~2018}, Austin, TX, USA, October 30 -- November 2, 2018}, publisher = {{IEEE}}, pages = {1--7}, doi = {10.23919/FMCAD.2018.8603013}, ) @article(KafleG17b, author = {B. Kafle and J. P. Gallagher}, year = {2017}, title = {Constraint specialisation in {H}orn clause verification}, journal = {Sci. Comput. Program.}, volume = {137}, pages = {125--140}, doi = {10.1016/j.scico.2017.01.002}, ) @inproceedings(Ko&13, author = {A. Komuravelli and A. Gurfinkel and S. Chaki and E. M. Clarke}, year = {2013}, title = {Automatic Abstraction in {SMT}-Based Unbounded Software Model Checking}, editor = {N. Sharygina and H. Veith}, booktitle = {Computer Aided Verification, Proceedings of the 25th International Conference {CAV}~'13, Saint Petersburg, Russia, July 13--19, 2013}, series = {Lecture Notes in Computer Science 8044}, publisher = {Springer}, pages = {846--862}, doi = {10.1007/978-3-642-39799-8\_59}, ) @inproceedings(Lei13, author = {K. R. M. Leino}, year = {2013}, title = {Developing Verified Programs with {D}afny}, booktitle = {Proceedings of the 2013 International Conference on Software Engineering}, series = {ICSE~'13}, publisher = {IEEE Press}, pages = {1488--1490}, doi = {10.1109/ICSE.2013.6606754}, ) @inproceedings(LeL00a, author = {M. Leuschel and H. Lehmann}, year = {2000}, title = {Coverability of Reset {P}etri Nets and Other Well-Structured Transition Systems by Partial Deduction.}, editor = {J. W. Lloyd}, booktitle = {Proceedings of the First International Conference on Computational Logic (CL 2000), London, UK, 24-28 July}, series = {Lecture Notes in Artificial Intelligence 1861}, publisher = {Springer-Verlag}, pages = {101--115}, doi = {10.1007/3-540-44957-4\_7}, ) @inproceedings(MeijerFP91, author = {E. Meijer and M. M. Fokkinga and R. Paterson}, year = {1991}, title = {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire}, editor = {J. Hughes}, booktitle = {Functional Programming Languages and Computer Architecture, 5th {ACM} Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings}, series = {Lecture Notes in Computer Science 523}, publisher = {Springer}, pages = {124--144}, doi = {10.1007/3540543961\_7}, ) @inproceedings(Me&07, author = {M{\'e}ndez-Lojo, M. and J. A. Navas and M. V. Hermenegildo}, year = {2008}, title = {A Flexible, {(C)LP}-Based Approach to the Analysis of Object-Oriented Programs}, booktitle = {17th International Symposium on Logic-Based Program Synthesis and Transformation, {LOPSTR}~'07, Kongens Lyngby, Denmark, August 23--24, 2007}, series = {Lecture Notes in Computer Science 4915}, publisher = {Springer}, pages = {154--168}, doi = {10.1007/978-3-540-78769-3\_11}, ) @inproceedings(MoF17, author = {D. Mordvinov and G. Fedyukovich}, year = {2017}, title = {Synchronizing Constrained {H}orn Clauses}, editor = {T. Eiter and D. Sands}, booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017}, series = {EPiC Series in Computing}, volume = {46}, publisher = {EasyChair}, pages = {338--355}, url = {http://www.easychair.org/publications/paper/340359}, ) @inproceedings(DeB08, author = {L. M. de Moura and Bj{\o}rner, N.}, year = {2008}, title = {Z3: {A}n Efficient {SMT} Solver}, booktitle = {Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS}~'08}, series = {Lecture Notes in Computer Science 4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3\_24}, ) @book(OderskySV11, author = {M. Odersky and L. Spoon and B. Venners}, year = {2011}, title = {Programming in {S}cala: {A} Comprehensive Step-by-Step Guide}, edition = {2nd}, publisher = {Artima Incorporation}, address = {Sunnyvale, CA, USA}, ) @inproceedings(Pe&98, author = {J. C. Peralta and J. P. Gallagher and H. Saglam}, year = {1998}, title = {Analysis of {I}mperative {P}rograms through {A}nalysis of {C}onstraint {L}ogic {P}rograms}, editor = {G. {L}evi}, booktitle = {Proceedings of the 5th {I}nternational {S}ymposium on {S}tatic {A}nalysis, {SAS}~'98}, series = {Lecture Notes in Computer Science 1503}, publisher = {Springer}, pages = {246--261}, doi = {10.1007/3-540-49727-7\_15}, ) @inproceedings(PeP89b, author = {A. Pettorossi and M. Proietti}, year = {1989}, title = {Decidability Results and Characterization of Strategies for the Development of Logic Pro\-grams}, editor = {G. Levi and M. Martelli}, booktitle = {Proceedings of the Sixth International Conference on Logic Pro\-gramming, Lisbon, Portugal}, publisher = {The MIT Press}, pages = {539--553}, ) @article(PhW16, author = {Tuan-Hung Pham and Andrew Gacek and Michael W. Whalen}, year = {2016}, title = {Reasoning About Algebraic Data Types with Abstractions}, journal = {J. Autom. Reason.}, volume = {57}, number = {4}, pages = {281--318}, doi = {10.1007/s10817-016-9368-2}, ) @incollection(PoR07, author = {A. Podelski and A. Rybalchenko}, year = {2007}, title = {{ARMC}: {T}he {L}ogical {C}hoice for {S}oftware {M}odel {C}hecking with {A}bstraction {R}efinement}, editor = {M. Hanus}, booktitle = {Practical Aspects of Declarative Languages, {PADL}~'07}, series = {Lecture Notes in Computer Science 4354}, publisher = {Springer}, pages = {245--259}, doi = {10.1007/978-3-540-69611-7\_16}, ) @article(PrP95a, author = {M. Proietti and A. Pettorossi}, year = {1995}, title = {Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Pro\-grams}, journal = {Theoretical Computer Science}, volume = {142}, number = {1}, pages = {89--124}, doi = {10.1016/0304-3975(94)00227-A}, ) @inproceedings(Ra&97, author = {Y. S. Ramakrishna and C. R. Ramakrishnan and I. V. Ramakrishnan and S. A. Smolka and T. Swift and D. S. Warren}, year = {1997}, title = {Efficient Model Checking Using Tabled Resolution}, booktitle = {Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97)}, series = {Lecture Notes in Computer Science 1254}, publisher = {Springer-Verlag}, pages = {143--154}, doi = {10.1007/3-540-63166-6\_16}, ) @techreport(Re&98, author = {S. Renault and A. Pettorossi and M. Proietti}, year = {1998}, title = {Design, Implementation, and Use of the {MAP} Transformation System}, type = {R}, number = {491}, institution = {IASI-CNR}, address = {Rome, Italy}, url = {http://www.iasi.cnr.it/~proietti/system.html}, ) @inproceedings(ReK15, author = {A. Reynolds and V. Kuncak}, year = {2015}, title = {Induction for {SMT} Solvers}, editor = {Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen}, booktitle = {Verification, Model Checking, and Abstract Interpretation, Proceedings of the 16th International Conference {VMCAI} 2015, Mumbai, India, January 12--14, 2015}, series = {Lecture Notes in Computer Science 8931}, publisher = {Springer}, pages = {80--98}, doi = {10.1007/978-3-662-46081-8_5}, ) @inproceedings(SuterDK10, author = {Ph. Suter and M. Dotta and V. Kuncak}, year = {2010}, title = {Decision procedures for algebraic data types with abstractions}, editor = {M. V. Hermenegildo and J. Palsberg}, booktitle = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23, 2010}, publisher = {{ACM}}, pages = {199--210}, doi = {10.1145/1706299.1706325}, ) @inproceedings(TaS84, author = {H. Tamaki and T. Sato}, year = {1984}, title = {Unfold/Fold Trans\-form\-ation of Logic Pro\-grams}, editor = {S.-{\r A}. T{{\"a}}rnlund}, booktitle = {Proceedings of the Second International Conference on Logic Pro\-gramming,~ICLP~'84}, publisher = {Uppsala University}, address = {Uppsala, Sweden}, pages = {127--138}, ) @inproceedings(Un&17, author = {H. Unno and S. Torii and H. Sakamoto}, year = {2017}, title = {Automating Induction for Solving {H}orn Clauses}, editor = {Rupak Majumdar and Viktor Kuncak}, booktitle = {Computer Aided Verification, Proceedings of the 29th International Conference {CAV}~'17, Heidelberg, Germany, Part {II}}, series = {Lecture Notes in Computer Science 10427}, publisher = {Springer}, pages = {571--591}, doi = {10.1007/978-3-319-63390-9_30}, ) @article(Wad90, author = {P. L. Wadler}, year = {1990}, title = {Deforestation: {T}rans\-forming Pro\-grams to Elim\-in\-ate Trees}, journal = {Theoretical Computer Science}, volume = {73}, pages = {231--248}, doi = {10.1016/0304-3975(90)90147-A}, )