@inproceedings(DBLP:conf/popl/AlbarghouthiDG16,
 author       = {Aws Albarghouthi and Isil Dillig and Arie Gurfinkel},
 year         = {2016},
 title        = {Maximal specification synthesis},
 editor       = {Bod{\'{\i}}k, Rastislav and Rupak Majumdar},
 booktitle    = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2016, St. Petersburg, FL, USA, January 20 - 22, 2016},
 publisher    = {{ACM}},
 pages        = {789--801},
 doi          = {10.1145/2837614.2837628},
)
@incollection(maxsat,
 author       = {Fahiem Bacchus and Matti J{\"a}rvisalo and Ruben Martins},
 year         = {2021},
 title        = {Maximum Satisfiability},
 editor       = {Armin Biere and Marijn Heule and {van Maaren}, Hans and Toby Walsh},
 booktitle    = {Handbook of Satisfiability},
 edition      = {2},
 series       = {Frontiers in Artificial Intelligence and Applications},
 publisher    = {IOS PRESS},
 address      = {Netherlands},
 pages        = {929 -- 991},
 doi          = {10.3233/FAIA201008},
)
@phdthesis(Beyene2015TemporalPV,
 author       = {Tewodros A. Beyene},
 year         = {2015},
 title        = {Temporal Program Verification and Synthesis as Horn Constraints Solving},
 school       = {TU Munich},
)
@inproceedings(BeyenePR13,
 author       = {Tewodros A. Beyene and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2013},
 title        = {Solving Existentially Quantified Horn Clauses},
 editor       = {Natasha Sharygina and Helmut Veith},
 booktitle    = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {869--882},
 doi          = {10.1007/978-3-642-39799-8\_61},
)
@inproceedings(BjornerGMR15,
 author       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2015},
 title        = {Horn Clause Solvers for Program Verification},
 editor       = {Lev D. Beklemishev and Andreas Blass and Nachum Dershowitz and Bernd Finkbeiner and Wolfram 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},
 volume       = {9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@inproceedings(BjornerMR13,
 author       = {Bj{\o}rner, Nikolaj and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2013},
 title        = {On Solving Universally Quantified Horn Clauses},
 editor       = {Francesco Logozzo and Manuel F{\"{a}}hndrich},
 booktitle    = {Static Analysis - 20th International Symposium, {SAS} 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7935},
 publisher    = {Springer},
 pages        = {105--125},
 doi          = {10.1007/978-3-642-38856-9\_8},
)
@inproceedings(Eldarica18,
 author       = {Hossein Hojjat and Philipp R{\"{u}}mmer},
 year         = {2018},
 title        = {The {ELDARICA} {Horn} Solver},
 editor       = {Bj{\o}rner, Nikolaj and Arie 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},
)
@inproceedings(HojjatRMCF16,
 author       = {Hossein Hojjat and Philipp R{\"{u}}mmer and Jedidiah McClurg and Pavol Cern{\'{y}} and Nate Foster},
 year         = {2016},
 title        = {Optimizing {Horn} solvers for network repair},
 editor       = {Ruzica Piskac and Muralidhar Talupur},
 booktitle    = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain View, CA, USA, October 3-6, 2016},
 publisher    = {{IEEE}},
 pages        = {73--80},
 doi          = {10.1109/FMCAD.2016.7886663},
)
@article(DBLP:journals/acta/LerouxRS16,
 author       = {J{\'{e}}r{\^{o}}me Leroux and Philipp R{\"{u}}mmer and Pavle Subotic},
 year         = {2016},
 title        = {Guiding Craig interpolation with domain-specific abstractions},
 journal      = {Acta Informatica},
 volume       = {53},
 number       = {4},
 pages        = {387--424},
 doi          = {10.1007/s00236-015-0236-z},
)
@inproceedings(DBLP:conf/pldi/SFMD21,
 author       = {Sumanth Prabhu S and Grigory Fedyukovich and Kumar Madhukar and Deepak D'Souza},
 year         = {2021},
 title        = {Specification synthesis with constrained Horn clauses},
 editor       = {Stephen N. Freund and Eran Yahav},
 booktitle    = {{PLDI} '21: 42nd {ACM} {SIGPLAN} International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021},
 publisher    = {{ACM}},
 pages        = {1203--1217},
 doi          = {10.1145/3453483.3454104},
)