@article(DBLP:journals/tcs/AfratiGT03, author = {Foto N. Afrati and Manolis Gergatsoulis and Francesca Toni}, year = {2003}, title = {Linearisability on {D}atalog programs}, journal = {Theor. Comput. Sci.}, volume = {308}, number = {1-3}, pages = {199--226}, doi = {10.1016/S0304-3975(02)00730-2}, ) @article(DBLP:journals/scp/BagnaraHZ08, author = {Roberto Bagnara and Patricia M. Hill and Enea Zaffanella}, year = {2008}, title = {The {Parma Polyhedra Library}: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems}, journal = {Sci. Comput. Program.}, volume = {72}, number = {1-2}, pages = {3--21}, doi = {10.1016/j.scico.2007.08.001}, ) @proceedings(DBLP:conf/tacas/2015, editor = {Christel Baier and Cesare Tinelli}, year = {2015}, title = {Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, {TACAS} 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0}, ) @inproceedings(DBLP:conf/tacas/000115, author = {Dirk Beyer}, year = {2015}, title = {Software Verification and Verifiable Witnesses - (Report on {SV-COMP} 2015)}, editor = {Baier and Tinelli}, pages = {401--416}, doi = {10.1007/978-3-662-46681-0\_31}, ) @inproceedings(DBLP:conf/sas/BjornerMR13, author = {Bj{\o}rner, Nikolaj and Kenneth L. McMillan and Andrey Rybalchenko}, year = {2013}, title = {On Solving Universally Quantified {H}orn Clauses}, editor = {Francesco Logozzo and Manuel F{\"a}hndrich}, booktitle = {SAS}, series = {LNCS}, volume = {7935}, publisher = {Springer}, pages = {105--125}, url = {http://dx.doi.org/10.1007/978-3-642-38856-9_8}, ) @inproceedings(DBLP:conf/popl/CousotC77, author = {Patrick Cousot and Radhia Cousot}, year = {1977}, title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints}, editor = {Robert M. Graham and Michael A. Harrison and Ravi Sethi}, booktitle = {POPL}, publisher = {ACM}, pages = {238--252}, url = {http://doi.acm.org/10.1145/512950.512973}, ) @inproceedings(DBLP:conf/popl/CousotH78, author = {Patrick Cousot and Nicolas Halbwachs}, year = {1978}, title = {{POPL}}, publisher = {{ACM} Press}, pages = {84--96}, doi = {10.1145/512760.512770}, url = {http://dl.acm.org/citation.cfm?id=512760}, ) @inproceedings(DBLP:conf/tacas/AngelisFPP14, author = {De Angelis, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2014}, title = {{VeriMAP}: A Tool for Verifying Programs through Transformations}, editor = {Erika {\'A}brah{\'a}m and Klaus Havelund}, booktitle = {TACAS}, series = {LNCS}, volume = {8413}, publisher = {Springer}, pages = {568--574}, url = {http://dx.doi.org/10.1007/978-3-642-54862-8_47}, ) @article(DBLP:journals/tplp/AngelisFPP15, author = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2015}, title = {Proving correctness of imperative programs by linearizing constrained {H}orn clauses}, journal = {{TPLP}}, volume = {15}, number = {4-5}, pages = {635--650}, doi = {10.1017/S1471068415000289}, ) @inproceedings(Dutertre:cav2014, author = {Bruno Dutertre}, year = {2014}, title = {Yices 2.2}, editor = {Armin Biere and Roderick Bloem}, booktitle = {Computer-Aided Verification (CAV'2014)}, series = {Lecture Notes in Computer Science}, volume = {8559}, publisher = {Springer}, pages = {737--744}, doi = {10.1007/978-3-319-08867-9\_49}, ) @article(DBLP:journals/ipl/EsparzaGKL11, author = {Javier Esparza and Pierre Ganty and Stefan Kiefer and Michael Luttenberger}, year = {2011}, title = {Parikh's theorem: {A} simple and direct automaton construction}, journal = {Inf. Process. Lett.}, volume = {111}, number = {12}, pages = {614--619}, doi = {10.1016/j.ipl.2011.03.019}, ) @inproceedings(DBLP:conf/stacs/EsparzaKL07, author = {Javier Esparza and Stefan Kiefer and Michael Luttenberger}, year = {2007}, title = {On Fixed Point Equations over Commutative Semirings}, booktitle = {{STACS} 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings}, series = {LNCS}, volume = {4393}, publisher = {Springer}, pages = {296--307}, doi = {10.1007/978-3-540-70918-3\_26}, ) @inproceedings(Gallagher-86, author = {J. P. Gallagher}, year = {1986}, title = {Transforming Logic Programs by Specialising Interpreters}, booktitle = {Proceedings of the 7th European Conference on Artificial Intelligence (ECAI-86), Brighton}, pages = {109--122}, ) @inproceedings(DBLP:conf/pepm/Gallagher93, author = {John P. Gallagher}, year = {1993}, title = {Tutorial on Specialisation of Logic Programs}, editor = {David A. Schmidt}, booktitle = {Proceedings of the {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'93, Copenhagen, Denmark, June 14-16, 1993}, publisher = {{ACM}}, pages = {88--98}, doi = {10.1145/154630.154640}, url = {http://dl.acm.org/citation.cfm?id=154630}, ) @inproceedings(DBLP:conf/tacas/GantyIK13, author = {Pierre Ganty and Radu Iosif and Kone\v{c}n\'{y}, Filip}, year = {2013}, title = {Underapproximation of Procedure Summaries for Integer Programs}, editor = {Nir Piterman and Scott A. Smolka}, booktitle = {{TACAS} 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7795}, publisher = {Springer}, pages = {245--259}, doi = {10.1007/978-3-642-36742-7\_18}, ) @inproceedings(DBLP:conf/tacas/GrebenshchikovGLPR12, author = {Sergey Grebenshchikov and Ashutosh Gupta and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko}, year = {2012}, title = {{HSF(C)}: A Software Verifier Based on {H}orn Clauses - (Competition Contribution)}, editor = {Cormac Flanagan and Barbara K{\"o}nig}, booktitle = {TACAS}, series = {LNCS}, volume = {7214}, publisher = {Springer}, pages = {549--551}, url = {http://dx.doi.org/10.1007/978-3-642-28756-5_46}, ) @inproceedings(DBLP:conf/pldi/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 = {{ACM} {SIGPLAN} {PLDI}}, publisher = {{ACM}}, pages = {405--416}, doi = {10.1145/2254064.2254112}, url = {http://dl.acm.org/citation.cfm?id=2254064}, ) @inproceedings(DBLP:conf/tacas/GurfinkelKN15, author = {Arie Gurfinkel and Temesghen Kahsai and Jorge A. Navas}, year = {2015}, title = {{SeaHorn}: {A} Framework for Verifying {C} Programs (Competition Contribution)}, editor = {Baier and Tinelli}, pages = {447--450}, doi = {10.1007/978-3-662-46681-0\_41}, ) @article(DBLP:journals/tplp/HermenegildoBCLMMP12, author = {Manuel V. Hermenegildo and Francisco Bueno and Manuel Carro and L{\'{o}}pez{-}Garc{\'{\i}}a, Pedro and Edison Mera and Jos{\'{e}} F. Morales and Germ{\'{a}}n Puebla}, year = {2012}, title = {An overview of {C}iao and its design philosophy}, journal = {{TPLP}}, volume = {12}, number = {1-2}, pages = {219--252}, doi = {10.1017/S1471068411000457}, ) @inproceedings(DBLP:conf/fm/HojjatKGIKR12, author = {Hossein Hojjat and Filip Konecn{\'{y}} and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp R{\"{u}}mmer}, year = {2012}, title = {A Verification Toolkit for Numerical Transition Systems - Tool Paper}, editor = {Dimitra Giannakopoulou and Dominique M{\'{e}}ry}, booktitle = {{FM}. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7436}, publisher = {Springer}, pages = {247--251}, doi = {10.1007/978-3-642-32759-9\_21}, ) @book(Jones-Gomard-Sestoft, author = {N. Jones and C.K. Gomard and P. Sestoft}, year = {1993}, title = {{P}artial {E}valuation and {A}utomatic {S}oftware {G}eneration}, publisher = {Prentice Hall}, ) @article(DBLP:journals/scp/Jones04, author = {Neil D. Jones}, year = {2004}, title = {Transformation by interpreter specialisation}, journal = {Sci. Comput. Program.}, volume = {52}, pages = {307--339}, doi = {10.1016/j.scico.2004.03.010}, ) @article(kafleG2015horn, author = {Bishoksan Kafle and John P Gallagher}, year = {2015}, title = {{H}orn clause verification with convex polyhedral abstraction and tree automata-based refinement}, journal = {Computer Languages, Systems \& Structures}, doi = {10.1016/j.cl.2015.11.001}, ) @inproceedings(DBLP:journals/corr/KafleGG15, author = {Bishoksan Kafle and John P. Gallagher and Pierre Ganty}, year = {2015}, title = {Decomposition by tree dimension in {H}orn clause verification}, editor = {Alexei Lisitsa and Andrei P. Nemytykh and Alberto Pettorossi}, booktitle = {{VPT}.}, series = {{EPTCS}}, volume = {199}, pages = {1--14}, doi = {10.4204/EPTCS.199.1}, ) @inproceedings(DBLP:conf/lopstr/Leuschel94, author = {Michael Leuschel}, year = {1994}, title = {Partial Evaluation of the ``Real Thing"}, editor = {Laurent Fribourg and Franco Turini}, booktitle = {{LOPSTR}, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {883}, publisher = {Springer}, pages = {122--137}, doi = {10.1007/3-540-58792-6\_8}, ) @inproceedings(DBLP:conf/pepm/LeuschelEVCF06, author = {Michael Leuschel and Daniel Elphick and Mauricio Varea and Stephen-John Craig and Marc Fontaine}, year = {2006}, title = {The {E}cce and {L}ogen partial evaluators and their web interfaces}, editor = {John Hatcliff and Frank Tip}, booktitle = {PEPM 2006}, publisher = {ACM}, pages = {88--94}, doi = {10.1145/1111542.1111557}, ) @article(DBLP:journals/iandc/LeuschelV14, author = {Michael Leuschel and Germ{\'{a}}n Vidal}, year = {2014}, title = {Fast offline partial evaluation of logic programs}, journal = {Inf. Comput.}, volume = {235}, pages = {70--97}, doi = {10.1016/j.ic.2014.01.005}, ) @article(DBLP:journals/iandc/LuttenbergerS16, author = {Michael Luttenberger and Maximilian Schlund}, year = {2016}, title = {Convergence of {N}ewton's Method over Commutative Semirings}, journal = {Inf. Comput.}, volume = {246}, pages = {43--61}, doi = {10.1016/j.ic.2015.11.008}, ) @techreport(McmillanR2013, author = {Kenneth L. McMillan and Andrey Rybalchenko}, year = {2013}, title = {Solving Constrained {H}orn Clauses using Interpolation}, type = {Technical Report}, institution = {Microsoft Research}, ) @inproceedings(DBLP:conf/cav/RummerHK13, author = {Philipp R{\"u}mmer and Hossein Hojjat and Viktor Kuncak}, year = {2013}, title = {Disjunctive Interpolants for {H}orn-Clause Verification}, editor = {Natasha Sharygina and Helmut Veith}, booktitle = {CAV}, series = {Lecture Notes in Computer Science}, volume = {8044}, publisher = {Springer}, pages = {347--363}, doi = {10.1007/978-3-642-39799-8}, url = {10.1007/978-3-642-39799-8\_24}, )