default search action
BibTeX records: Cesare Tinelli
@inproceedings{DBLP:conf/cav/JohannsenNDISTVR24, author = {Chris Johannsen and Karthik Nukala and Rohit Dureja and Ahmed Irfan and Natarajan Shankar and Cesare Tinelli and Moshe Y. Vardi and Kristin Yvonne Rozier}, editor = {Arie Gurfinkel and Vijay Ganesh}, title = {The MoXI Model Exchange Tool Suite}, booktitle = {Computer Aided Verification - 36th International Conference, {CAV} 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {14681}, pages = {203--218}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-65627-9\_10}, doi = {10.1007/978-3-031-65627-9\_10}, timestamp = {Fri, 02 Aug 2024 11:58:28 +0200}, biburl = {https://dblp.org/rec/conf/cav/JohannsenNDISTVR24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fm/BarrettTBNPRZ24, author = {Clark W. Barrett and Cesare Tinelli and Haniel Barbosa and Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar}, editor = {Andre Platzer and Kristin Yvonne Rozier and Matteo Pradella and Matteo Rossi}, title = {Satisfiability Modulo Theories: {A} Beginner's Tutorial}, booktitle = {Formal Methods - 26th International Symposium, {FM} 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {14934}, pages = {571--596}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-71177-0\_31}, doi = {10.1007/978-3-031-71177-0\_31}, timestamp = {Fri, 20 Sep 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fm/BarrettTBNPRZ24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ijcar/TsiskaridzeBT24, author = {Nestan Tsiskaridze and Clark W. Barrett and Cesare Tinelli}, editor = {Christoph Benzm{\"{u}}ller and Marijn J. H. Heule and Renate A. Schmidt}, title = {Generalized Optimization Modulo Theories}, booktitle = {Automated Reasoning - 12th International Joint Conference, {IJCAR} 2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {14739}, pages = {458--479}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-63498-7\_27}, doi = {10.1007/978-3-031-63498-7\_27}, timestamp = {Fri, 02 Aug 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/ijcar/TsiskaridzeBT24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/Mohamed0TB24, author = {Mudathir Mohamed and Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, editor = {Nikolaj S. Bj{\o}rner and Marijn Heule and Andrei Voronkov}, title = {Verifying {SQL} queries using theories of tables and relations}, booktitle = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024}, series = {EPiC Series in Computing}, volume = {100}, pages = {445--463}, publisher = {EasyChair}, year = {2024}, url = {https://doi.org/10.29007/rlt7}, doi = {10.29007/RLT7}, timestamp = {Tue, 25 Jun 2024 16:52:02 +0200}, biburl = {https://dblp.org/rec/conf/lpar/Mohamed0TB24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sat/Tinelli24, author = {Cesare Tinelli}, editor = {Supratik Chakraborty and Jie{-}Hong Roland Jiang}, title = {Scalable Proof Production and Checking in {SMT} (Invited Talk)}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2024, August 21-24, 2024, Pune, India}, series = {LIPIcs}, volume = {305}, pages = {2:1--2:2}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2024}, url = {https://doi.org/10.4230/LIPIcs.SAT.2024.2}, doi = {10.4230/LIPICS.SAT.2024.2}, timestamp = {Wed, 21 Aug 2024 22:46:00 +0200}, biburl = {https://dblp.org/rec/conf/sat/Tinelli24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tacas/LachnittFARBNBT24, author = {Hanna Lachnitt and Mathias Fleury and Leni Aniva and Andrew Reynolds and Haniel Barbosa and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {Bernd Finkbeiner and Laura Kov{\'{a}}cs}, title = {IsaRare: Automatic Verification of {SMT} Rewrites in Isabelle/HOL}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, {TACAS} 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {14570}, pages = {311--330}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-57246-3\_17}, doi = {10.1007/978-3-031-57246-3\_17}, timestamp = {Sat, 08 Jun 2024 13:13:56 +0200}, biburl = {https://dblp.org/rec/conf/tacas/LachnittFARBNBT24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2404-16122, author = {Nestan Tsiskaridze and Clark W. Barrett and Cesare Tinelli}, title = {Generalized Optimization Modulo Theories}, journal = {CoRR}, volume = {abs/2404.16122}, year = {2024}, url = {https://doi.org/10.48550/arXiv.2404.16122}, doi = {10.48550/ARXIV.2404.16122}, eprinttype = {arXiv}, eprint = {2404.16122}, timestamp = {Mon, 03 Jun 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2404-16122.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2405-03057, author = {Mudathir Mohamed and Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, title = {Verifying {SQL} Queries using Theories of Tables and Relations}, journal = {CoRR}, volume = {abs/2405.03057}, year = {2024}, url = {https://doi.org/10.48550/arXiv.2405.03057}, doi = {10.48550/ARXIV.2405.03057}, eprinttype = {arXiv}, eprint = {2405.03057}, timestamp = {Fri, 07 Jun 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2405-03057.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/cacm/BarbosaBCDKLNNOPRTZ23, author = {Haniel Barbosa and Clark W. Barrett and Byron Cook and Bruno Dutertre and Gereon Kremer and Hanna Lachnitt and Aina Niemetz and Andres N{\"{o}}tzli and Alex Ozdemir and Mathias Preiner and Andrew Reynolds and Cesare Tinelli and Yoni Zohar}, title = {Generating and Exploiting Automated Reasoning Proof Certificates}, journal = {Commun. {ACM}}, volume = {66}, number = {10}, pages = {86--95}, year = {2023}, url = {https://doi.org/10.1145/3587692}, doi = {10.1145/3587692}, timestamp = {Tue, 07 May 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/cacm/BarbosaBCDKLNNOPRTZ23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/AbateBBDKKPRT23, author = {Alessandro Abate and Haniel Barbosa and Clark W. Barrett and Cristina David and Pascal Kesseli and Daniel Kroening and Elizabeth Polgreen and Andrew Reynolds and Cesare Tinelli}, title = {Synthesising Programs with Non-trivial Constants}, journal = {J. Autom. Reason.}, volume = {67}, number = {2}, pages = {19}, year = {2023}, url = {https://doi.org/10.1007/s10817-023-09664-4}, doi = {10.1007/S10817-023-09664-4}, timestamp = {Tue, 12 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/AbateBBDKKPRT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/ShengNRZDGPQBT23, author = {Ying Sheng and Andres N{\"{o}}tzli and Andrew Reynolds and Yoni Zohar and David L. Dill and Wolfgang Grieskamp and Junkil Park and Shaz Qadeer and Clark W. Barrett and Cesare Tinelli}, title = {Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences}, journal = {J. Autom. Reason.}, volume = {67}, number = {3}, pages = {32}, year = {2023}, url = {https://doi.org/10.1007/s10817-023-09682-2}, doi = {10.1007/S10817-023-09682-2}, timestamp = {Sun, 12 Nov 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/jar/ShengNRZDGPQBT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/ShengZRRBT23, author = {Ying Sheng and Yoni Zohar and Christophe Ringeissen and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, title = {Combining Stable Infiniteness and (Strong) Politeness}, journal = {J. Autom. Reason.}, volume = {67}, number = {4}, pages = {34}, year = {2023}, url = {https://doi.org/10.1007/s10817-023-09684-0}, doi = {10.1007/S10817-023-09684-0}, timestamp = {Sun, 12 Nov 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/jar/ShengZRRBT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/OzdemirKTB23, author = {Alex Ozdemir and Gereon Kremer and Cesare Tinelli and Clark W. Barrett}, editor = {Constantin Enea and Akash Lal}, title = {Satisfiability Modulo Finite Fields}, booktitle = {Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {13965}, pages = {163--186}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-37703-7\_8}, doi = {10.1007/978-3-031-37703-7\_8}, timestamp = {Tue, 12 Sep 2023 07:57:21 +0200}, biburl = {https://dblp.org/rec/conf/cav/OzdemirKTB23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/RozierSTV23, author = {Kristin Y. Rozier and Natarajan Shankar and Cesare Tinelli and Moshe Y. Vardi}, editor = {Alexander Nadel and Kristin Yvonne Rozier}, title = {Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2023, Ames, IA, USA, October 24-27, 2023}, pages = {1}, publisher = {{IEEE}}, year = {2023}, url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0\_4}, doi = {10.34727/2023/ISBN.978-3-85448-060-0\_4}, timestamp = {Wed, 13 Dec 2023 14:38:51 +0100}, biburl = {https://dblp.org/rec/conf/fmcad/RozierSTV23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/MohamedRBT23, author = {Abdalrhman Mohamed and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Alexander Nadel and Kristin Yvonne Rozier}, title = {A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2023, Ames, IA, USA, October 24-27, 2023}, pages = {189--198}, publisher = {{IEEE}}, year = {2023}, url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0\_27}, doi = {10.34727/2023/ISBN.978-3-85448-060-0\_27}, timestamp = {Wed, 13 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fmcad/MohamedRBT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/WilsonNRCTB23, author = {Amalee Wilson and Andres N{\"{o}}tzli and Andrew Reynolds and Byron Cook and Cesare Tinelli and Clark W. Barrett}, editor = {Alexander Nadel and Kristin Yvonne Rozier}, title = {Partitioning Strategies for Distributed {SMT} Solving}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2023, Ames, IA, USA, October 24-27, 2023}, pages = {199--208}, publisher = {{IEEE}}, year = {2023}, url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0\_28}, doi = {10.34727/2023/ISBN.978-3-85448-060-0\_28}, timestamp = {Wed, 13 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fmcad/WilsonNRCTB23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/LarrazLYACT23, author = {Daniel Larraz and Robert Lorch and Moosa Yahyazadeh and M. Fareed Arif and Omar Chowdhury and Cesare Tinelli}, editor = {Alexander Nadel and Kristin Yvonne Rozier}, title = {{CRV:} Automated Cyber-Resiliency Reasoning for System Design Models}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2023, Ames, IA, USA, October 24-27, 2023}, pages = {209--220}, publisher = {{IEEE}}, year = {2023}, url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0\_29}, doi = {10.34727/2023/ISBN.978-3-85448-060-0\_29}, timestamp = {Wed, 13 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fmcad/LarrazLYACT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/frocos/EkiciVZTB23, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Cesare Tinelli and Clark W. Barrett}, editor = {Uli Sattler and Martin Suda}, title = {Formal Verification of Bit-Vector Invertibility Conditions in Coq}, booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {14279}, pages = {41--59}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-43369-6\_3}, doi = {10.1007/978-3-031-43369-6\_3}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/frocos/EkiciVZTB23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/BarbosaK0VTB23, author = {Haniel Barbosa and Chantal Keller and Andrew Reynolds and Arjun Viswanathan and Cesare Tinelli and Clark W. Barrett}, editor = {Ruzica Piskac and Andrei Voronkov}, title = {An Interactive {SMT} Tactic in Coq using Abductive Reasoning}, booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023}, series = {EPiC Series in Computing}, volume = {94}, pages = {11--22}, publisher = {EasyChair}, year = {2023}, url = {https://doi.org/10.29007/432m}, doi = {10.29007/432M}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lpar/BarbosaK0VTB23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/smt/LachnittFA0BNBT23, author = {Hanna Lachnitt and Mathias Fleury and Leni Aniva and Andrew Reynolds and Haniel Barbosa and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {St{\'{e}}phane Graham{-}Lengrand and Mathias Preiner}, title = {Automatic Verification of {SMT} Rewrites in Isabelle/HOL}, booktitle = {Proceedings of the 21st International Workshop on Satisfiability Modulo Theories {(SMT} 2023) co-located with the 29th International Conference on Automated Deduction {(CADE} 2023), Rome, Italy, July, 5-6, 2023}, series = {{CEUR} Workshop Proceedings}, volume = {3429}, pages = {78}, publisher = {CEUR-WS.org}, year = {2023}, url = {https://ceur-ws.org/Vol-3429/abstract14.pdf}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/smt/LachnittFA0BNBT23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/cade/2023, editor = {Brigitte Pientka and Cesare Tinelli}, title = {Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {14132}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-38499-8}, doi = {10.1007/978-3-031-38499-8}, isbn = {978-3-031-38498-1}, timestamp = {Tue, 12 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/2023.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2306-05854, author = {Amalee Wilson and Andres N{\"{o}}tzli and Andrew Reynolds and Byron Cook and Cesare Tinelli and Clark W. Barrett}, title = {Partitioning Strategies for Distributed {SMT} Solving}, journal = {CoRR}, volume = {abs/2306.05854}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2306.05854}, doi = {10.48550/ARXIV.2306.05854}, eprinttype = {arXiv}, eprint = {2306.05854}, timestamp = {Wed, 14 Jun 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2306-05854.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iacr/OzdemirKTB23, author = {Alex Ozdemir and Gereon Kremer and Cesare Tinelli and Clark W. Barrett}, title = {Satisfiability Modulo Finite Fields}, journal = {{IACR} Cryptol. ePrint Arch.}, pages = {91}, year = {2023}, url = {https://eprint.iacr.org/2023/091}, timestamp = {Tue, 28 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iacr/OzdemirKTB23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BarbosaRKLNNOPV22, author = {Haniel Barbosa and Andrew Reynolds and Gereon Kremer and Hanna Lachnitt and Aina Niemetz and Andres N{\"{o}}tzli and Alex Ozdemir and Mathias Preiner and Arjun Viswanathan and Scott Viteri and Yoni Zohar and Cesare Tinelli and Clark W. Barrett}, editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson}, title = {Flexible Proof Production in an Industrial-Strength {SMT} Solver}, booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13385}, pages = {15--35}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-10769-6\_3}, doi = {10.1007/978-3-031-10769-6\_3}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/BarbosaRKLNNOPV22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/KremerRBT22, author = {Gereon Kremer and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson}, title = {Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 {SMT} Solver (System Description)}, booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13385}, pages = {95--105}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-10769-6\_7}, doi = {10.1007/978-3-031-10769-6\_7}, timestamp = {Mon, 24 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/KremerRBT22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ShengNRZDGPQBT22, author = {Ying Sheng and Andres N{\"{o}}tzli and Andrew Reynolds and Yoni Zohar and David L. Dill and Wolfgang Grieskamp and Junkil Park and Shaz Qadeer and Clark W. Barrett and Cesare Tinelli}, editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson}, title = {Reasoning About Vectors Using an {SMT} Theory of Sequences}, booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13385}, pages = {125--143}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-10769-6\_9}, doi = {10.1007/978-3-031-10769-6\_9}, timestamp = {Wed, 07 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cade/ShengNRZDGPQBT22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/NotzliRBBT22, author = {Andres N{\"{o}}tzli and Andrew Reynolds and Haniel Barbosa and Clark W. Barrett and Cesare Tinelli}, editor = {Sharon Shoham and Yakir Vizel}, title = {Even Faster Conflicts and Lazier Reductions for String Solvers}, booktitle = {Computer Aided Verification - 34th International Conference, {CAV} 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {13372}, pages = {205--226}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-13188-2\_11}, doi = {10.1007/978-3-031-13188-2\_11}, timestamp = {Thu, 25 Aug 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/NotzliRBBT22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/NotzliBNPRBT22, author = {Andres N{\"{o}}tzli and Haniel Barbosa and Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Alberto Griggio and Neha Rungta}, title = {Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language}, booktitle = {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022, Trento, Italy, October 17-21, 2022}, pages = {65--74}, publisher = {{IEEE}}, year = {2022}, url = {https://doi.org/10.34727/2022/isbn.978-3-85448-053-2\_12}, doi = {10.34727/2022/ISBN.978-3-85448-053-2\_12}, timestamp = {Sun, 12 Nov 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/fmcad/NotzliBNPRBT22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22, author = {Haniel Barbosa and Clark W. Barrett and Martin Brain and Gereon Kremer and Hanna Lachnitt and Makai Mann and Abdalrhman Mohamed and Mudathir Mohamed and Aina Niemetz and Andres N{\"{o}}tzli and Alex Ozdemir and Mathias Preiner and Andrew Reynolds and Ying Sheng and Cesare Tinelli and Yoni Zohar}, editor = {Dana Fisman and Grigore Rosu}, title = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, {TACAS} 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {13243}, pages = {415--442}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-030-99524-9\_24}, doi = {10.1007/978-3-030-99524-9\_24}, timestamp = {Fri, 29 Apr 2022 14:50:36 +0200}, biburl = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/vmcai/ZoharIMNNPRBT22, author = {Yoni Zohar and Ahmed Irfan and Makai Mann and Aina Niemetz and Andres N{\"{o}}tzli and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Bernd Finkbeiner and Thomas Wies}, title = {Bit-Precise Reasoning via Int-Blasting}, booktitle = {Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, {VMCAI} 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13182}, pages = {496--518}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-030-94583-1\_24}, doi = {10.1007/978-3-030-94583-1\_24}, timestamp = {Fri, 21 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/vmcai/ZoharIMNNPRBT22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2205-08095, author = {Ying Sheng and Andres N{\"{o}}tzli and Andrew Reynolds and Yoni Zohar and David L. Dill and Wolfgang Grieskamp and Junkil Park and Shaz Qadeer and Clark W. Barrett and Cesare Tinelli}, title = {Reasoning About Vectors using an {SMT} Theory of Sequences}, journal = {CoRR}, volume = {abs/2205.08095}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2205.08095}, doi = {10.48550/ARXIV.2205.08095}, eprinttype = {arXiv}, eprint = {2205.08095}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2205-08095.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2205-09082, author = {Daniel Larraz and Cesare Tinelli}, title = {Realizability Checking of Contracts with Kind 2}, journal = {CoRR}, volume = {abs/2205.09082}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2205.09082}, doi = {10.48550/ARXIV.2205.09082}, eprinttype = {arXiv}, eprint = {2205.09082}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2205-09082.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/fmsd/NiemetzPRBT21, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, title = {On solving quantified bit-vector constraints using invertibility conditions}, journal = {Formal Methods Syst. Des.}, volume = {57}, number = {1}, pages = {87--115}, year = {2021}, url = {https://doi.org/10.1007/s10703-020-00359-9}, doi = {10.1007/S10703-020-00359-9}, timestamp = {Thu, 29 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/fmsd/NiemetzPRBT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/NiemetzP0ZBT21, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, title = {Towards Satisfiability Modulo Parametric Bit-vectors}, journal = {J. Autom. Reason.}, volume = {65}, number = {7}, pages = {1001--1025}, year = {2021}, url = {https://doi.org/10.1007/s10817-021-09598-9}, doi = {10.1007/S10817-021-09598-9}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/NiemetzP0ZBT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/systems/MengLSMISPPHAYV21, author = {Baoluo Meng and Daniel Larraz and Kit Siu and Abha Moitra and John Interrante and William Smith and Saswata Paul and Daniel Prince and Heber Herencia{-}Zapana and M. Fareed Arif and Moosa Yahyazadeh and Vidhya Tekken Valapil and Michael Durling and Cesare Tinelli and Omar Chowdhury}, title = {{VERDICT:} {A} Language and Framework for Engineering Cyber Resilient and Safe System}, journal = {Syst.}, volume = {9}, number = {1}, pages = {18}, year = {2021}, url = {https://doi.org/10.3390/systems9010018}, doi = {10.3390/SYSTEMS9010018}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/systems/MengLSMISPPHAYV21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/0007ZRRBT21, author = {Ying Sheng and Yoni Zohar and Christophe Ringeissen and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Andr{\'{e}} Platzer and Geoff Sutcliffe}, title = {Politeness and Stable Infiniteness: Stronger Together}, booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12699}, pages = {148--165}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-79876-5\_9}, doi = {10.1007/978-3-030-79876-5\_9}, timestamp = {Thu, 29 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/0007ZRRBT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmics/LarrazLT21, author = {Daniel Larraz and Micka{\"{e}}l Laurent and Cesare Tinelli}, editor = {Alberto Lluch{-}Lafuente and Anastasia Mavridou}, title = {Merit and Blame Assignment with Kind 2}, booktitle = {Formal Methods for Industrial Critical Systems - 26th International Conference, {FMICS} 2021, Paris, France, August 24-26, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12863}, pages = {212--220}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-85248-1\_14}, doi = {10.1007/978-3-030-85248-1\_14}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmics/LarrazLT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sat/MannWZSIBDGTB21, author = {Makai Mann and Amalee Wilson and Yoni Zohar and Lindsey Stuntz and Ahmed Irfan and Kristopher Brown and Caleb Donovick and Allison Guman and Cesare Tinelli and Clark W. Barrett}, editor = {Chu{-}Min Li and Felip Many{\`{a}}}, title = {Smt-Switch: {A} Solver-Agnostic {C++} {API} for {SMT} Solving}, booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12831}, pages = {377--386}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-80223-3\_26}, doi = {10.1007/978-3-030-80223-3\_26}, timestamp = {Thu, 29 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/sat/MannWZSIBDGTB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tacas/NiemetzPRBT21, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Jan Friso Groote and Kim Guldstrand Larsen}, title = {Syntax-Guided Quantifier Instantiation}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, {TACAS} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {12652}, pages = {145--163}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-72013-1\_8}, doi = {10.1007/978-3-030-72013-1\_8}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/tacas/NiemetzPRBT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@incollection{DBLP:series/faia/BarrettSST21, author = {Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli}, editor = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh}, title = {Satisfiability Modulo Theories}, booktitle = {Handbook of Satisfiability - Second Edition}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {336}, pages = {1267--1329}, publisher = {{IOS} Press}, year = {2021}, url = {https://doi.org/10.3233/FAIA201017}, doi = {10.3233/FAIA201017}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/series/faia/BarrettSST21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2104-11738, author = {Ying Sheng and Yoni Zohar and Christophe Ringeissen and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, title = {Politeness and Stable Infiniteness: Stronger Together}, journal = {CoRR}, volume = {abs/2104.11738}, year = {2021}, url = {https://arxiv.org/abs/2104.11738}, eprinttype = {arXiv}, eprint = {2104.11738}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2104-11738.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2105-06575, author = {Daniel Larraz and Micka{\"{e}}l Laurent and Cesare Tinelli}, title = {Merit and Blame Assignment with Kind 2}, journal = {CoRR}, volume = {abs/2105.06575}, year = {2021}, url = {https://arxiv.org/abs/2105.06575}, eprinttype = {arXiv}, eprint = {2105.06575}, timestamp = {Tue, 18 May 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2105-06575.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/BiereTW20, author = {Armin Biere and Cesare Tinelli and Christoph Weidenbach}, title = {Preface to the Special Issue on Automated Reasoning Systems}, journal = {J. Autom. Reason.}, volume = {64}, number = {3}, pages = {361--362}, year = {2020}, url = {https://doi.org/10.1007/s10817-019-09531-1}, doi = {10.1007/S10817-019-09531-1}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/BiereTW20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jsc/DavenportEGST20, author = {James H. Davenport and Matthew England and Alberto Griggio and Thomas Sturm and Cesare Tinelli}, title = {Symbolic computation and satisfiability checking}, journal = {J. Symb. Comput.}, volume = {100}, pages = {1--10}, year = {2020}, url = {https://doi.org/10.1016/j.jsc.2019.07.017}, doi = {10.1016/J.JSC.2019.07.017}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jsc/DavenportEGST20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ReynoldsBLT20, author = {Andrew Reynolds and Haniel Barbosa and Daniel Larraz and Cesare Tinelli}, editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans}, title = {Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis}, booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12166}, pages = {141--160}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-51074-9\_9}, doi = {10.1007/978-3-030-51074-9\_9}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ReynoldsBLT20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ReynoldsNBT20, author = {Andrew Reynolds and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans}, title = {A Decision Procedure for String to Code Point Conversion}, booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12166}, pages = {218--237}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-51074-9\_13}, doi = {10.1007/978-3-030-51074-9\_13}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ReynoldsNBT20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/dlog/BaaderKT20, author = {Franz Baader and Patrick Koopmann and Cesare Tinelli}, editor = {Stefan Borgwardt and Thomas Meyer}, title = {First Results on How to Certify Subsumptions Computed by the {EL} Reasoner {ELK} Using the Logical Framework with Side Conditions}, booktitle = {Proceedings of the 33rd International Workshop on Description Logics {(DL} 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning {(KR} 2020), Online Event [Rhodes, Greece], September 12th to 14th, 2020}, series = {{CEUR} Workshop Proceedings}, volume = {2663}, publisher = {CEUR-WS.org}, year = {2020}, url = {https://ceur-ws.org/Vol-2663/paper-5.pdf}, timestamp = {Fri, 10 Mar 2023 16:23:17 +0100}, biburl = {https://dblp.org/rec/conf/dlog/BaaderKT20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/ArifLERCT20, author = {M. Fareed Arif and Daniel Larraz and Mitziu Echeverria and Andrew Reynolds and Omar Chowdhury and Cesare Tinelli}, title = {{SYSLITE:} Syntax-Guided Synthesis of {PLTL} Formulas from Finite Traces}, booktitle = {2020 Formal Methods in Computer Aided Design, {FMCAD} 2020, Haifa, Israel, September 21-24, 2020}, pages = {93--103}, publisher = {{IEEE}}, year = {2020}, url = {https://doi.org/10.34727/2020/isbn.978-3-85448-042-6\_16}, doi = {10.34727/2020/ISBN.978-3-85448-042-6\_16}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/ArifLERCT20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/ReynoldsNBT20, author = {Andrew Reynolds and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, title = {Reductions for Strings and Regular Expressions Revisited}, booktitle = {2020 Formal Methods in Computer Aided Design, {FMCAD} 2020, Haifa, Israel, September 21-24, 2020}, pages = {225--235}, publisher = {{IEEE}}, year = {2020}, url = {https://doi.org/10.34727/2020/isbn.978-3-85448-042-6\_30}, doi = {10.34727/2020/ISBN.978-3-85448-042-6\_30}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/ReynoldsNBT20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/smt/MannWTB20, author = {Makai Mann and Amalee Wilson and Cesare Tinelli and Clark W. Barrett}, editor = {Fran{\c{c}}ois Bobot and Tjark Weber}, title = {Smt-Switch: {A} Solver-agnostic {C++} {API} for {SMT} Solving}, booktitle = {Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning {(IJCAR} 2020), Online (initially located in Paris, France), July 5-6, 2020}, series = {{CEUR} Workshop Proceedings}, volume = {2854}, pages = {48--58}, publisher = {CEUR-WS.org}, year = {2020}, url = {https://ceur-ws.org/Vol-2854/short3.pdf}, timestamp = {Fri, 10 Mar 2023 16:22:48 +0100}, biburl = {https://dblp.org/rec/conf/smt/MannWTB20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2007-01374, author = {Makai Mann and Amalee Wilson and Cesare Tinelli and Clark W. Barrett}, title = {Smt-Switch: a solver-agnostic {C++} {API} for {SMT} Solving}, journal = {CoRR}, volume = {abs/2007.01374}, year = {2020}, url = {https://arxiv.org/abs/2007.01374}, eprinttype = {arXiv}, eprint = {2007.01374}, timestamp = {Mon, 06 Jul 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2007-01374.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/fmsd/ReynoldsKTBD19, author = {Andrew Reynolds and Viktor Kuncak and Cesare Tinelli and Clark W. Barrett and Morgan Deters}, title = {Refutation-based synthesis in {SMT}}, journal = {Formal Methods Syst. Des.}, volume = {55}, number = {2}, pages = {73--102}, year = {2019}, url = {https://doi.org/10.1007/s10703-017-0270-2}, doi = {10.1007/S10703-017-0270-2}, timestamp = {Mon, 25 Jul 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/fmsd/ReynoldsKTBD19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/birthday/LutzSTTW19, author = {Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni{-}Yasmin Turhan and Frank Wolter}, editor = {Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni{-}Yasmin Turhan and Frank Wolter}, title = {A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction}, booktitle = {Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {11560}, pages = {1--14}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-22102-7\_1}, doi = {10.1007/978-3-030-22102-7\_1}, timestamp = {Sun, 17 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/birthday/LutzSTTW19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/birthday/BonacinaFRT19, author = {Maria Paola Bonacina and Pascal Fontaine and Christophe Ringeissen and Cesare Tinelli}, editor = {Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni{-}Yasmin Turhan and Frank Wolter}, title = {Theory Combination: Beyond Equality Sharing}, booktitle = {Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {11560}, pages = {57--89}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-22102-7\_3}, doi = {10.1007/978-3-030-22102-7\_3}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/birthday/BonacinaFRT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BarbosaROTB19, author = {Haniel Barbosa and Andrew Reynolds and Daniel El Ouraoui and Cesare Tinelli and Clark W. Barrett}, editor = {Pascal Fontaine}, title = {Extending {SMT} Solvers to Higher-Order Logic}, booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11716}, pages = {35--54}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-29436-6\_3}, doi = {10.1007/978-3-030-29436-6\_3}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/BarbosaROTB19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/NiemetzPRZBT19, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, editor = {Pascal Fontaine}, title = {Towards Bit-Width-Independent Proofs in {SMT} Solvers}, booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11716}, pages = {366--384}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-29436-6\_22}, doi = {10.1007/978-3-030-29436-6\_22}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/NiemetzPRZBT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ReynoldsNBT19, author = {Andrew Reynolds and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {Isil Dillig and Serdar Tasiran}, title = {High-Level Abstractions for Simplifying Extended String Constraints in {SMT}}, booktitle = {Computer Aided Verification - 31st International Conference, {CAV} 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {11562}, pages = {23--42}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-25543-5\_2}, doi = {10.1007/978-3-030-25543-5\_2}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/ReynoldsNBT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ReynoldsBNBT19, author = {Andrew Reynolds and Haniel Barbosa and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, editor = {Isil Dillig and Serdar Tasiran}, title = {cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis}, booktitle = {Computer Aided Verification - 31st International Conference, {CAV} 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {11562}, pages = {74--83}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-25543-5\_5}, doi = {10.1007/978-3-030-25543-5\_5}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/ReynoldsBNBT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/BrainNPRBT19, author = {Martin Brain and Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Isil Dillig and Serdar Tasiran}, title = {Invertibility Conditions for Floating-Point Formulas}, booktitle = {Computer Aided Verification - 31st International Conference, {CAV} 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {11562}, pages = {116--136}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-25543-5\_8}, doi = {10.1007/978-3-030-25543-5\_8}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/BrainNPRBT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/BarbosaRLT19, author = {Haniel Barbosa and Andrew Reynolds and Daniel Larraz and Cesare Tinelli}, editor = {Clark W. Barrett and Jin Yang}, title = {Extending enumerative function synthesis via SMT-driven classification}, booktitle = {2019 Formal Methods in Computer Aided Design, {FMCAD} 2019, San Jose, CA, USA, October 22-25, 2019}, pages = {212--220}, publisher = {{IEEE}}, year = {2019}, url = {https://doi.org/10.23919/FMCAD.2019.8894267}, doi = {10.23919/FMCAD.2019.8894267}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/BarbosaRLT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sat/NotzliRBNPBT19, author = {Andres N{\"{o}}tzli and Andrew Reynolds and Haniel Barbosa and Aina Niemetz and Mathias Preiner and Clark W. Barrett and Cesare Tinelli}, editor = {Mikol{\'{a}}s Janota and In{\^{e}}s Lynce}, title = {Syntax-Guided Rewrite Rule Enumeration for {SMT} Solvers}, booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2019 - 22nd International Conference, {SAT} 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11628}, pages = {279--297}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-24258-9\_20}, doi = {10.1007/978-3-030-24258-9\_20}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/sat/NotzliRBNPBT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09478, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, editor = {Giselle Reis and Haniel Barbosa}, title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {18--26}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.4}, doi = {10.4204/EPTCS.301.4}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09478.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/birthday/2019baader, editor = {Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni{-}Yasmin Turhan and Frank Wolter}, title = {Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {11560}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-22102-7}, doi = {10.1007/978-3-030-22102-7}, isbn = {978-3-030-22101-0}, timestamp = {Mon, 29 Jul 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/birthday/2019baader.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1905-10434, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, title = {Towards Bit-Width-Independent Proofs in {SMT} Solvers}, journal = {CoRR}, volume = {abs/1905.10434}, year = {2019}, url = {http://arxiv.org/abs/1905.10434}, eprinttype = {arXiv}, eprint = {1905.10434}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1905-10434.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1907-10175, author = {Andrew Reynolds and Haniel Barbosa and Andres N{\"{o}}tzli and Clark W. Barrett and Cesare Tinelli}, title = {{CVC4SY} for SyGuS-COMP 2019}, journal = {CoRR}, volume = {abs/1907.10175}, year = {2019}, url = {http://arxiv.org/abs/1907.10175}, eprinttype = {arXiv}, eprint = {1907.10175}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1907-10175.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/dagstuhl-reports/FuhsRST19, author = {Carsten Fuhs and Philipp R{\"{u}}mmer and Renate A. Schmidt and Cesare Tinelli}, title = {Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)}, journal = {Dagstuhl Reports}, volume = {9}, number = {9}, pages = {23--44}, year = {2019}, url = {https://doi.org/10.4230/DagRep.9.9.23}, doi = {10.4230/DAGREP.9.9.23}, timestamp = {Fri, 21 Feb 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/dagstuhl-reports/FuhsRST19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/lmcs/BansalBRT18, author = {Kshitij Bansal and Clark W. Barrett and Andrew Reynolds and Cesare Tinelli}, title = {Reasoning with Finite Sets and Cardinality Constraints in {SMT}}, journal = {Log. Methods Comput. Sci.}, volume = {14}, number = {4}, year = {2018}, url = {https://doi.org/10.23638/LMCS-14(4:12)2018}, doi = {10.23638/LMCS-14(4:12)2018}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/lmcs/BansalBRT18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ReynoldsVBTB18, author = {Andrew Reynolds and Arjun Viswanathan and Haniel Barbosa and Cesare Tinelli and Clark W. Barrett}, editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani}, title = {Datatypes with Shared Selectors}, booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10900}, pages = {591--608}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-94205-6\_39}, doi = {10.1007/978-3-319-94205-6\_39}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ReynoldsVBTB18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/NiemetzPRBT18, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Hana Chockler and Georg Weissenbacher}, title = {Solving Quantified Bit-Vectors Using Invertibility Conditions}, booktitle = {Computer Aided Verification - 30th International Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {10982}, pages = {236--255}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-96142-2\_16}, doi = {10.1007/978-3-319-96142-2\_16}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/NiemetzPRBT18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@incollection{DBLP:reference/mc/BarrettT18, author = {Clark W. Barrett and Cesare Tinelli}, editor = {Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem}, title = {Satisfiability Modulo Theories}, booktitle = {Handbook of Model Checking}, pages = {305--343}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-10575-8\_11}, doi = {10.1007/978-3-319-10575-8\_11}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/reference/mc/BarrettT18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1804-05025, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, title = {On Solving Quantified Bit-Vectors using Invertibility Conditions}, journal = {CoRR}, volume = {abs/1804.05025}, year = {2018}, url = {http://arxiv.org/abs/1804.05025}, eprinttype = {arXiv}, eprint = {1804.05025}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1804-05025.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1806-08775, author = {Clark W. Barrett and Haniel Barbosa and Martin Brain and Duligur Ibeling and Tim King and Paul Meng and Aina Niemetz and Andres N{\"{o}}tzli and Mathias Preiner and Andrew Reynolds and Cesare Tinelli}, title = {{CVC4} at the {SMT} Competition 2018}, journal = {CoRR}, volume = {abs/1806.08775}, year = {2018}, url = {http://arxiv.org/abs/1806.08775}, eprinttype = {arXiv}, eprint = {1806.08775}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1806-08775.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/acta/BaierT17, author = {Christel Baier and Cesare Tinelli}, title = {Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems {(TACAS} 2015)}, journal = {Acta Informatica}, volume = {54}, number = {8}, pages = {727--728}, year = {2017}, url = {https://doi.org/10.1007/s00236-017-0298-1}, doi = {10.1007/S00236-017-0298-1}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/acta/BaierT17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/sttt/BaierT17, author = {Christel Baier and Cesare Tinelli}, title = {Some advances in tools and algorithms for the construction and analysis of systems}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {19}, number = {6}, pages = {649--652}, year = {2017}, url = {https://doi.org/10.1007/s10009-017-0471-4}, doi = {10.1007/S10009-017-0471-4}, timestamp = {Sun, 04 Aug 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/sttt/BaierT17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tplp/ReynoldsTB17, author = {Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, title = {Constraint solving for finite model finding in {SMT} solvers}, journal = {Theory Pract. Log. Program.}, volume = {17}, number = {4}, pages = {516--558}, year = {2017}, url = {https://doi.org/10.1017/S1471068417000175}, doi = {10.1017/S1471068417000175}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/tplp/ReynoldsTB17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/MengRTB17, author = {Baoluo Meng and Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, editor = {Leonardo de Moura}, title = {Relational Constraint Solving in {SMT}}, booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10395}, pages = {148--165}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-63046-5\_10}, doi = {10.1007/978-3-319-63046-5\_10}, timestamp = {Thu, 29 Sep 2022 08:36:56 +0200}, biburl = {https://dblp.org/rec/conf/cade/MengRTB17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/EkiciMTKKRB17, author = {Burak Ekici and Alain Mebsout and Cesare Tinelli and Chantal Keller and Guy Katz and Andrew Reynolds and Clark W. Barrett}, editor = {Rupak Majumdar and Viktor Kuncak}, title = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq}, booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {10427}, pages = {126--133}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-63390-9\_7}, doi = {10.1007/978-3-319-63390-9\_7}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/EkiciMTKKRB17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ReynoldsWBBLT17, author = {Andrew Reynolds and Maverick Woo and Clark W. Barrett and David Brumley and Tianyi Liang and Cesare Tinelli}, editor = {Rupak Majumdar and Viktor Kuncak}, title = {Scaling Up {DPLL(T)} String Solvers Using Context-Dependent Simplification}, booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {10427}, pages = {453--474}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-63390-9\_24}, doi = {10.1007/978-3-319-63390-9\_24}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/ReynoldsWBBLT17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/frocos/ReynoldsTJB17, author = {Andrew Reynolds and Cesare Tinelli and Dejan Jovanovic and Clark W. Barrett}, editor = {Clare Dixon and Marcelo Finger}, title = {Designing Theory Solvers with Extensions}, booktitle = {Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10483}, pages = {22--40}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-66167-4\_2}, doi = {10.1007/978-3-319-66167-4\_2}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/frocos/ReynoldsTJB17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/nfm/WagnerMTCS17, author = {Lucas G. Wagner and Alain Mebsout and Cesare Tinelli and Darren D. Cofer and Konrad Slind}, editor = {Clark W. Barrett and Misty D. Davies and Temesghen Kahsai}, title = {Qualification of a Model Checker for Avionics Software Verification}, booktitle = {{NASA} Formal Methods - 9th International Symposium, {NFM} 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10227}, pages = {404--419}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-57288-8\_29}, doi = {10.1007/978-3-319-57288-8\_29}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/nfm/WagnerMTCS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1711-10641, author = {Andrew Reynolds and Cesare Tinelli}, editor = {Dana Fisman and Swen Jacobs}, title = {SyGuS Techniques in the Core of an {SMT} Solver}, booktitle = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017}, series = {{EPTCS}}, volume = {260}, pages = {81--96}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.260.8}, doi = {10.4204/EPTCS.260.8}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1711-10641.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/BansalBRT17, author = {Kshitij Bansal and Clark W. Barrett and Andrew Reynolds and Cesare Tinelli}, title = {A New Decision Procedure for Finite Sets and Cardinality Constraints in {SMT}}, journal = {CoRR}, volume = {abs/1702.06259}, year = {2017}, url = {http://arxiv.org/abs/1702.06259}, eprinttype = {arXiv}, eprint = {1702.06259}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BansalBRT17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/ReynoldsTB17, author = {Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, title = {Constraint Solving for Finite Model Finding in {SMT} Solvers}, journal = {CoRR}, volume = {abs/1706.00096}, year = {2017}, url = {http://arxiv.org/abs/1706.00096}, eprinttype = {arXiv}, eprint = {1706.00096}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/ReynoldsTB17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/dagstuhl-reports/BlanchetteFST17, author = {Jasmin Christian Blanchette and Carsten Fuhs and Viorica Sofronie{-}Stokkermans and Cesare Tinelli}, title = {Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}, journal = {Dagstuhl Reports}, volume = {7}, number = {9}, pages = {26--46}, year = {2017}, url = {https://doi.org/10.4230/DagRep.7.9.26}, doi = {10.4230/DAGREP.7.9.26}, timestamp = {Mon, 12 Mar 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/dagstuhl-reports/BlanchetteFST17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/fmsd/LiangRTTBD16, author = {Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze and Cesare Tinelli and Clark W. Barrett and Morgan Deters}, title = {An efficient {SMT} solver for string constraints}, journal = {Formal Methods Syst. Des.}, volume = {48}, number = {3}, pages = {206--234}, year = {2016}, url = {https://doi.org/10.1007/s10703-016-0247-6}, doi = {10.1007/S10703-016-0247-6}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/fmsd/LiangRTTBD16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BansalRBT16, author = {Kshitij Bansal and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli}, editor = {Nicola Olivetti and Ashish Tiwari}, title = {A New Decision Procedure for Finite Sets and Cardinality Constraints in {SMT}}, booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9706}, pages = {82--98}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-40229-1\_7}, doi = {10.1007/978-3-319-40229-1\_7}, timestamp = {Mon, 26 Jun 2023 20:45:22 +0200}, biburl = {https://dblp.org/rec/conf/cade/BansalRBT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ReynoldsBCT16, author = {Andrew Reynolds and Jasmin Christian Blanchette and Simon Cruanes and Cesare Tinelli}, editor = {Nicola Olivetti and Ashish Tiwari}, title = {Model Finding for Recursive Functions in {SMT}}, booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9706}, pages = {133--151}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-40229-1\_10}, doi = {10.1007/978-3-319-40229-1\_10}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ReynoldsBCT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ChampionMST16, author = {Adrien Champion and Alain Mebsout and Christoph Sticksel and Cesare Tinelli}, editor = {Swarat Chaudhuri and Azadeh Farzan}, title = {The Kind 2 Model Checker}, booktitle = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {9780}, pages = {510--517}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-41540-6\_29}, doi = {10.1007/978-3-319-41540-6\_29}, timestamp = {Tue, 14 May 2019 10:00:43 +0200}, biburl = {https://dblp.org/rec/conf/cav/ChampionMST16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/KatzBTRH16, author = {Guy Katz and Clark W. Barrett and Cesare Tinelli and Andrew Reynolds and Liana Hadarean}, editor = {Ruzica Piskac and Muralidhar Talupur}, title = {Lazy proofs for DPLL(T)-based {SMT} solvers}, booktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain View, CA, USA, October 3-6, 2016}, pages = {93--100}, publisher = {{IEEE}}, year = {2016}, url = {https://doi.org/10.1109/FMCAD.2016.7886666}, doi = {10.1109/FMCAD.2016.7886666}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/KatzBTRH16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/MebsoutT16, author = {Alain Mebsout and Cesare Tinelli}, editor = {Ruzica Piskac and Muralidhar Talupur}, title = {Proof certificates for SMT-based model checkers for infinite-state systems}, booktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain View, CA, USA, October 3-6, 2016}, pages = {117--124}, publisher = {{IEEE}}, year = {2016}, url = {https://doi.org/10.1109/FMCAD.2016.7886669}, doi = {10.1109/FMCAD.2016.7886669}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/MebsoutT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/hotsos/BarrettTDLRT16, author = {Clark W. Barrett and Cesare Tinelli and Morgan Deters and Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze}, editor = {William L. Scherlis and David Brumley}, title = {Efficient solving of string constraints for security analysis}, booktitle = {Proceedings of the Symposium and Bootcamp on the Science of Security, Pittsburgh, PA, USA, April 19-21, 2016}, pages = {4--6}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2898375.2898393}, doi = {10.1145/2898375.2898393}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/hotsos/BarrettTDLRT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sefm/ChampionGKT16, author = {Adrien Champion and Arie Gurfinkel and Temesghen Kahsai and Cesare Tinelli}, editor = {Rocco De Nicola and Eva K{\"{u}}hn}, title = {CoCoSpec: {A} Mode-Aware Contract Language for Reactive Systems}, booktitle = {Software Engineering and Formal Methods - 14th International Conference, {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9763}, pages = {347--366}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-41591-8\_24}, doi = {10.1007/978-3-319-41591-8\_24}, timestamp = {Tue, 15 Nov 2022 15:22:36 +0100}, biburl = {https://dblp.org/rec/conf/sefm/ChampionGKT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/EkiciKKMRT16, author = {Burak Ekici and Guy Katz and Chantal Keller and Alain Mebsout and Andrew J. Reynolds and Cesare Tinelli}, editor = {Jasmin Christian Blanchette and Cezary Kaliszyk}, title = {Extending SMTCoq, a Certified Checker for {SMT} (Extended Abstract)}, booktitle = {Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016}, series = {{EPTCS}}, volume = {210}, pages = {21--29}, year = {2016}, url = {https://doi.org/10.4204/EPTCS.210.5}, doi = {10.4204/EPTCS.210.5}, timestamp = {Wed, 16 Mar 2022 23:52:32 +0100}, biburl = {https://dblp.org/rec/journals/corr/EkiciKKMRT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/arith/BrainTRW15, author = {Martin Brain and Cesare Tinelli and Philipp R{\"{u}}mmer and Thomas Wahl}, title = {An Automatable Formal Semantics for {IEEE-754} Floating-Point Arithmetic}, booktitle = {22nd {IEEE} Symposium on Computer Arithmetic, {ARITH} 2015, Lyon, France, June 22-24, 2015}, pages = {160--167}, publisher = {{IEEE}}, year = {2015}, url = {https://doi.org/10.1109/ARITH.2015.26}, doi = {10.1109/ARITH.2015.26}, timestamp = {Wed, 16 Oct 2019 14:14:53 +0200}, biburl = {https://dblp.org/rec/conf/arith/BrainTRW15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ReynoldsDKTB15, author = {Andrew Reynolds and Morgan Deters and Viktor Kuncak and Cesare Tinelli and Clark W. Barrett}, editor = {Daniel Kroening and Corina S. Pasareanu}, title = {Counterexample-Guided Quantifier Instantiation for Synthesis in {SMT}}, booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {9207}, pages = {198--216}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-21668-3\_12}, doi = {10.1007/978-3-319-21668-3\_12}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/ReynoldsDKTB15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/frocos/LiangTRTB15, author = {Tianyi Liang and Nestan Tsiskaridze and Andrew Reynolds and Cesare Tinelli and Clark W. Barrett}, editor = {Carsten Lutz and Silvio Ranise}, title = {A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings}, booktitle = {Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9322}, pages = {135--150}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-24246-0\_9}, doi = {10.1007/978-3-319-24246-0\_9}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/frocos/LiangTRTB15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/HadareanBRTD15, author = {Liana Hadarean and Clark W. Barrett and Andrew Reynolds and Cesare Tinelli and Morgan Deters}, editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov}, title = {Fine Grained {SMT} Proofs for the Theory of Fixed-Width Bit-Vectors}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9450}, pages = {340--355}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-662-48899-7\_24}, doi = {10.1007/978-3-662-48899-7\_24}, timestamp = {Mon, 03 Jan 2022 22:31:30 +0100}, biburl = {https://dblp.org/rec/conf/lpar/HadareanBRTD15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/tacas/2015, editor = {Christel Baier and Cesare Tinelli}, 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}, year = {2015}, url = {https://doi.org/10.1007/978-3-662-46681-0}, doi = {10.1007/978-3-662-46681-0}, isbn = {978-3-662-46680-3}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/tacas/2015.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/ReynoldsDKBT15, author = {Andrew Reynolds and Morgan Deters and Viktor Kuncak and Clark W. Barrett and Cesare Tinelli}, title = {On Counterexample Guided Quantifier Instantiation for Synthesis in {CVC4}}, journal = {CoRR}, volume = {abs/1502.04464}, year = {2015}, url = {http://arxiv.org/abs/1502.04464}, eprinttype = {arXiv}, eprint = {1502.04464}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/ReynoldsDKBT15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/StumpST14, author = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli}, editor = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach}, title = {StarExec: {A} Cross-Community Infrastructure for Logic Solving}, booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 19-22, 2014. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8562}, pages = {367--373}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08587-6\_28}, doi = {10.1007/978-3-319-08587-6\_28}, timestamp = {Fri, 09 Apr 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/StumpST14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/LiangRTBD14, author = {Tianyi Liang and Andrew Reynolds and Cesare Tinelli and Clark W. Barrett and Morgan Deters}, editor = {Armin Biere and Roderick Bloem}, title = {A {DPLL(T)} Theory Solver for a Theory of Strings and Regular Expressions}, booktitle = {Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8559}, pages = {646--662}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08867-9\_43}, doi = {10.1007/978-3-319-08867-9\_43}, timestamp = {Mon, 03 Jan 2022 22:13:44 +0100}, biburl = {https://dblp.org/rec/conf/cav/LiangRTBD14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/HadareanBJBT14, author = {Liana Hadarean and Kshitij Bansal and Dejan Jovanovic and Clark W. Barrett and Cesare Tinelli}, editor = {Armin Biere and Roderick Bloem}, title = {A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors}, booktitle = {Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8559}, pages = {680--695}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08867-9\_45}, doi = {10.1007/978-3-319-08867-9\_45}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/HadareanBJBT14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/DetersR0BT14, author = {Morgan Deters and Andrew Reynolds and Tim King and Clark W. Barrett and Cesare Tinelli}, title = {A tour of {CVC4:} How it works, and how to use it}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland, October 21-24, 2014}, pages = {7}, publisher = {{IEEE}}, year = {2014}, url = {https://doi.org/10.1109/FMCAD.2014.6987586}, doi = {10.1109/FMCAD.2014.6987586}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/DetersR0BT14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/0001BT14, author = {Tim King and Clark W. Barrett and Cesare Tinelli}, title = {Leveraging linear and mixed integer programming for {SMT}}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland, October 21-24, 2014}, pages = {139--146}, publisher = {{IEEE}}, year = {2014}, url = {https://doi.org/10.1109/FMCAD.2014.6987606}, doi = {10.1109/FMCAD.2014.6987606}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/0001BT14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/ReynoldsTM14, author = {Andrew Reynolds and Cesare Tinelli and Leonardo Mendon{\c{c}}a de Moura}, title = {Finding conflicting instances of quantified formulas in {SMT}}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland, October 21-24, 2014}, pages = {195--202}, publisher = {{IEEE}}, year = {2014}, url = {https://doi.org/10.1109/FMCAD.2014.6987613}, doi = {10.1109/FMCAD.2014.6987613}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/ReynoldsTM14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/smt/0001BT14, author = {Tim King and Clark W. Barrett and Cesare Tinelli}, editor = {Philipp R{\"{u}}mmer and Christoph M. Wintersteiger}, title = {Leveraging Linear and Mixed Integer Programming for {SMT}}, booktitle = {Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, {SMT} 2014, affiliated with the 26th International Conference on Computer Aided Verification {(CAV} 2014), the 7th International Joint Conference on Automated Reasoning {(IJCAR} 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing {(SAT} 2014), Vienna, Austria, July 17-18, 2014}, series = {{CEUR} Workshop Proceedings}, volume = {1163}, pages = {65}, publisher = {CEUR-WS.org}, year = {2014}, url = {https://ceur-ws.org/Vol-1163/paper-10.pdf}, timestamp = {Fri, 10 Mar 2023 16:22:48 +0100}, biburl = {https://dblp.org/rec/conf/smt/0001BT14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/fmsd/StumpORHT13, author = {Aaron Stump and Duckki Oe and Andrew Reynolds and Liana Hadarean and Cesare Tinelli}, title = {{SMT} proof checking using a logical framework}, journal = {Formal Methods Syst. Des.}, volume = {42}, number = {1}, pages = {91--118}, year = {2013}, url = {https://doi.org/10.1007/s10703-012-0163-3}, doi = {10.1007/S10703-012-0163-3}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/fmsd/StumpORHT13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ReynoldsTGKDB13, author = {Andrew Reynolds and Cesare Tinelli and Amit Goel and Sava Krstic and Morgan Deters and Clark W. Barrett}, editor = {Maria Paola Bonacina}, title = {Quantifier Instantiation Techniques for Finite Model Finding in {SMT}}, booktitle = {Automated Deduction - {CADE-24} - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7898}, pages = {377--391}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-642-38574-2\_26}, doi = {10.1007/978-3-642-38574-2\_26}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ReynoldsTGKDB13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/ReynoldsTGK13, author = {Andrew Reynolds and Cesare Tinelli and Amit Goel and Sava Krstic}, editor = {Natasha Sharygina and Helmut Veith}, title = {Finite Model Finding in {SMT}}, 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}, pages = {640--655}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-642-39799-8\_42}, doi = {10.1007/978-3-642-39799-8\_42}, timestamp = {Wed, 07 Dec 2022 23:12:58 +0100}, biburl = {https://dblp.org/rec/conf/cav/ReynoldsTGK13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/nfm/GarocheKT13, author = {Pierre{-}Lo{\"{\i}}c Garoche and Temesghen Kahsai and Cesare Tinelli}, editor = {Guillaume Brat and Neha Rungta and Arnaud Venet}, title = {Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers}, booktitle = {{NASA} Formal Methods, 5th International Symposium, {NFM} 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7871}, pages = {139--154}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-642-38088-4\_10}, doi = {10.1007/978-3-642-38088-4\_10}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/nfm/GarocheKT13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1111-5652, author = {Alexander Fuchs and Amit Goel and Jim Grundy and Sava Krstic and Cesare Tinelli}, title = {Ground interpolation for the theory of equality}, journal = {Log. Methods Comput. Sci.}, volume = {8}, number = {1}, year = {2012}, url = {https://doi.org/10.2168/LMCS-8(1:6)2012}, doi = {10.2168/LMCS-8(1:6)2012}, timestamp = {Thu, 25 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-5652.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jsc/BaumgartnerPT12, author = {Peter Baumgartner and Bj{\"{o}}rn Pelzer and Cesare Tinelli}, title = {Model Evolution with equality - Revised and implemented}, journal = {J. Symb. Comput.}, volume = {47}, number = {9}, pages = {1011--1045}, year = {2012}, url = {https://doi.org/10.1016/j.jsc.2011.12.031}, doi = {10.1016/J.JSC.2011.12.031}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/jsc/BaumgartnerPT12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/StumpST12, author = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli}, editor = {Vladimir Klebanov and Bernhard Beckert and Armin Biere and Geoff Sutcliffe}, title = {Introducing StarExec: a Cross-Community Infrastructure for Logic Solving}, booktitle = {Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {873}, pages = {2}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-873/papers/inv\_1.pdf}, timestamp = {Fri, 10 Mar 2023 16:23:14 +0100}, biburl = {https://dblp.org/rec/conf/cade/StumpST12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/LiangT12, author = {Tianyi Liang and Cesare Tinelli}, editor = {Pascal Fontaine and Renate A. Schmidt and Stephan Schulz}, title = {Exploiting parallelism in the {ME} calculus}, booktitle = {Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30 - July 1, 2012}, series = {EPiC Series in Computing}, volume = {21}, pages = {96--108}, publisher = {EasyChair}, year = {2012}, url = {https://doi.org/10.29007/v1f2}, doi = {10.29007/V1F2}, timestamp = {Sun, 15 Aug 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/LiangT12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/nfm/Tinelli12, author = {Cesare Tinelli}, editor = {Alwyn Goodloe and Suzette Person}, title = {SMT-Based Model Checking}, booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7226}, pages = {1}, publisher = {Springer}, year = {2012}, url = {https://doi.org/10.1007/978-3-642-28891-3\_1}, doi = {10.1007/978-3-642-28891-3\_1}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/nfm/Tinelli12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/nfm/KahsaiGTW12, author = {Temesghen Kahsai and Pierre{-}Lo{\"{\i}}c Garoche and Cesare Tinelli and Mike Whalen}, editor = {Alwyn Goodloe and Suzette Person}, title = {Incremental Verification with Mode Variable Invariants in State Machines}, booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7226}, pages = {388--402}, publisher = {Springer}, year = {2012}, url = {https://doi.org/10.1007/978-3-642-28891-3\_35}, doi = {10.1007/978-3-642-28891-3\_35}, timestamp = {Thu, 15 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/nfm/KahsaiGTW12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/StumpRTLEOZ12, author = {Aaron Stump and Andrew Reynolds and Cesare Tinelli and Austin Laugesen and Harley Eades III and Corey Oliver and Ruoyu Zhang}, editor = {David Pichardie and Tjark Weber}, title = {{LFSC} for {SMT} Proofs: Work in Progress}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {21--27}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper1.pdf}, timestamp = {Fri, 10 Mar 2023 16:22:21 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/StumpRTLEOZ12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/cade/2010emsqms, editor = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli}, title = {Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, {EMSQMS} 2010, Edinburgh, UK, July 20, 2010}, series = {EPiC Series in Computing}, volume = {6}, publisher = {EasyChair}, year = {2012}, url = {https://easychair.org/publications/volume/EMSQMS\_2010}, timestamp = {Fri, 13 Aug 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/2010emsqms.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1205-3758, author = {Pierre{-}Lo{\"{\i}}c Garoche and Temesghen Kahsai and Cesare Tinelli}, title = {Invariant stream generators using automatic abstract transformers based on a decidable logic}, journal = {CoRR}, volume = {abs/1205.3758}, year = {2012}, url = {http://arxiv.org/abs/1205.3758}, eprinttype = {arXiv}, eprint = {1205.3758}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1205-3758.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BaumgartnerT11, author = {Peter Baumgartner and Cesare Tinelli}, editor = {Nikolaj S. Bj{\o}rner and Viorica Sofronie{-}Stokkermans}, title = {Model Evolution with Equality Modulo Built-in Theories}, booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6803}, pages = {85--100}, publisher = {Springer}, year = {2011}, url = {https://doi.org/10.1007/978-3-642-22438-6\_9}, doi = {10.1007/978-3-642-22438-6\_9}, timestamp = {Mon, 28 Aug 2023 21:17:45 +0200}, biburl = {https://dblp.org/rec/conf/cade/BaumgartnerT11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/BarrettCDHJKRT11, author = {Clark W. Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, title = {{CVC4}}, booktitle = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6806}, pages = {171--177}, publisher = {Springer}, year = {2011}, url = {https://doi.org/10.1007/978-3-642-22110-1\_14}, doi = {10.1007/978-3-642-22110-1\_14}, timestamp = {Tue, 27 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cav/BarrettCDHJKRT11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/nfm/KahsaiGT11, author = {Temesghen Kahsai and Yeting Ge and Cesare Tinelli}, editor = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi}, title = {Instantiation-Based Invariant Discovery}, booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6617}, pages = {192--206}, publisher = {Springer}, year = {2011}, url = {https://doi.org/10.1007/978-3-642-20398-5\_15}, doi = {10.1007/978-3-642-20398-5\_15}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/nfm/KahsaiGT11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0372, author = {Temesghen Kahsai and Cesare Tinelli}, editor = {Jiri Barnat and Keijo Heljanko}, title = {PKind: {A} parallel k-induction based model checker}, booktitle = {Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, {PDMC} 2011, Snowbird, Utah, USA, July 14, 2011}, series = {{EPTCS}}, volume = {72}, pages = {55--62}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.72.6}, doi = {10.4204/EPTCS.72.6}, timestamp = {Fri, 09 Apr 2021 18:27:20 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0372.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/frocos/2011, editor = {Cesare Tinelli and Viorica Sofronie{-}Stokkermans}, title = {Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbr{\"{u}}cken, Germany, October 5-7, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6989}, publisher = {Springer}, year = {2011}, url = {https://doi.org/10.1007/978-3-642-24364-6}, doi = {10.1007/978-3-642-24364-6}, isbn = {978-3-642-24363-9}, timestamp = {Tue, 14 May 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/frocos/2011.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/hvc/BarrettMRST10, author = {Clark W. Barrett and Leonardo Mendon{\c{c}}a de Moura and Silvio Ranise and Aaron Stump and Cesare Tinelli}, editor = {Sharon Barner and Ian G. Harris and Daniel Kroening and Orna Raz}, title = {The {SMT-LIB} Initiative and the Rise of {SMT} - {(HVC} 2010 Award Talk)}, booktitle = {Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, {HVC} 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {6504}, pages = {3}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-19583-9\_2}, doi = {10.1007/978-3-642-19583-9\_2}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/hvc/BarrettMRST10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/wollic/Tinelli10, author = {Cesare Tinelli}, editor = {Anuj Dawar and Ruy J. G. B. de Queiroz}, title = {Foundations of Satisfiability Modulo Theories}, booktitle = {Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6188}, pages = {58}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-13824-9\_6}, doi = {10.1007/978-3-642-13824-9\_6}, timestamp = {Tue, 14 May 2019 10:00:40 +0200}, biburl = {https://dblp.org/rec/conf/wollic/Tinelli10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/amai/GeBT09, author = {Yeting Ge and Clark W. Barrett and Cesare Tinelli}, title = {Solving quantified verification conditions using satisfiability modulo theories}, journal = {Ann. Math. Artif. Intell.}, volume = {55}, number = {1-2}, pages = {101--122}, year = {2009}, url = {https://doi.org/10.1007/s10472-009-9153-6}, doi = {10.1007/S10472-009-9153-6}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/amai/GeBT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/japll/BaumgartnerFNT09, author = {Peter Baumgartner and Alexander Fuchs and Hans de Nivelle and Cesare Tinelli}, title = {Computing finite models by reduction to function-free clause logic}, journal = {J. Appl. Log.}, volume = {7}, number = {1}, pages = {58--74}, year = {2009}, url = {https://doi.org/10.1016/j.jal.2007.07.005}, doi = {10.1016/J.JAL.2007.07.005}, timestamp = {Tue, 16 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/japll/BaumgartnerFNT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/GoelKT09, author = {Amit Goel and Sava Krstic and Cesare Tinelli}, editor = {Renate A. Schmidt}, title = {Ground Interpolation for Combined Theories}, booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5663}, pages = {183--198}, publisher = {Springer}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-02959-2\_16}, doi = {10.1007/978-3-642-02959-2\_16}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/GoelKT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tacas/FuchsGGKT09, author = {Alexander Fuchs and Amit Goel and Jim Grundy and Sava Krstic and Cesare Tinelli}, editor = {Stefan Kowalewski and Anna Philippou}, title = {Ground Interpolation for the Theory of Equality}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, {TACAS} 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2009, York, UK, March 22-29, 2009. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5505}, pages = {413--427}, publisher = {Springer}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-00768-2\_34}, doi = {10.1007/978-3-642-00768-2\_34}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/tacas/FuchsGGKT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@incollection{DBLP:series/faia/BarrettSST09, author = {Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli}, editor = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh}, title = {Satisfiability Modulo Theories}, booktitle = {Handbook of Satisfiability}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {185}, pages = {825--885}, publisher = {{IOS} Press}, year = {2009}, url = {https://doi.org/10.3233/978-1-58603-929-5-825}, doi = {10.3233/978-1-58603-929-5-825}, timestamp = {Fri, 06 May 2022 08:00:40 +0200}, biburl = {https://dblp.org/rec/series/faia/BarrettSST09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/ai/BaumgartnerT08, author = {Peter Baumgartner and Cesare Tinelli}, title = {The model evolution calculus as a first-order {DPLL} method}, journal = {Artif. Intell.}, volume = {172}, number = {4-5}, pages = {591--632}, year = {2008}, url = {https://doi.org/10.1016/j.artint.2007.09.005}, doi = {10.1016/J.ARTINT.2007.09.005}, timestamp = {Sun, 12 Nov 2017 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/ai/BaumgartnerT08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fmcad/HagenT08, author = {George Hagen and Cesare Tinelli}, editor = {Alessandro Cimatti and Robert B. Jones}, title = {Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques}, booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2008, Portland, Oregon, USA, 17-20 November 2008}, pages = {1--9}, publisher = {{IEEE}}, year = {2008}, url = {https://doi.org/10.1109/FMCAD.2008.ECP.19}, doi = {10.1109/FMCAD.2008.ECP.19}, timestamp = {Wed, 16 Oct 2019 14:14:56 +0200}, biburl = {https://dblp.org/rec/conf/fmcad/HagenT08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/BaumgartnerFT08, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov}, title = {{(LIA)} - Model Evolution with Linear Integer Arithmetic Constraints}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, {LPAR} 2008, Doha, Qatar, November 22-27, 2008. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5330}, pages = {258--273}, publisher = {Springer}, year = {2008}, url = {https://doi.org/10.1007/978-3-540-89439-1\_19}, doi = {10.1007/978-3-540-89439-1\_19}, timestamp = {Tue, 14 May 2019 10:00:55 +0200}, biburl = {https://dblp.org/rec/conf/lpar/BaumgartnerFT08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jsat/BarrettST07, author = {Clark W. Barrett and Igor Shikanian and Cesare Tinelli}, title = {An Abstract Decision Procedure for a Theory of Inductive Data Types}, journal = {J. Satisf. Boolean Model. Comput.}, volume = {3}, number = {1-2}, pages = {21--46}, year = {2007}, url = {https://doi.org/10.3233/sat190028}, doi = {10.3233/SAT190028}, timestamp = {Mon, 17 Aug 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jsat/BarrettST07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/GeBT07, author = {Yeting Ge and Clark W. Barrett and Cesare Tinelli}, editor = {Frank Pfenning}, title = {Solving Quantified Verification Conditions Using Satisfiability Modulo Theories}, booktitle = {Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4603}, pages = {167--182}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-73595-3\_12}, doi = {10.1007/978-3-540-73595-3\_12}, timestamp = {Mon, 24 Jun 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/GeBT07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/Tinelli07, author = {Cesare Tinelli}, editor = {Bernhard Beckert}, title = {Trends and Challenges in Satisfiability Modulo Theories}, booktitle = {Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007}, series = {{CEUR} Workshop Proceedings}, volume = {259}, publisher = {CEUR-WS.org}, year = {2007}, url = {https://ceur-ws.org/Vol-259/paper03.pdf}, timestamp = {Fri, 10 Mar 2023 16:23:14 +0100}, biburl = {https://dblp.org/rec/conf/cade/Tinelli07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/BarrettT07, author = {Clark W. Barrett and Cesare Tinelli}, editor = {Werner Damm and Holger Hermanns}, title = {{CVC3}}, booktitle = {Computer Aided Verification, 19th International Conference, {CAV} 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4590}, pages = {298--302}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-73368-3\_34}, doi = {10.1007/978-3-540-73368-3\_34}, timestamp = {Sat, 30 Sep 2023 09:35:55 +0200}, biburl = {https://dblp.org/rec/conf/cav/BarrettT07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tableaux/Tinelli07, author = {Cesare Tinelli}, editor = {Nicola Olivetti}, title = {An Abstract Framework for Satisfiability Modulo Theories}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, {TABLEAUX} 2007, Aix en Provence, France, July 3-6, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4548}, pages = {10}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-73099-6\_3}, doi = {10.1007/978-3-540-73099-6\_3}, timestamp = {Tue, 14 May 2019 10:00:54 +0200}, biburl = {https://dblp.org/rec/conf/tableaux/Tinelli07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tacas/KrsticGGT07, author = {Sava Krstic and Amit Goel and Jim Grundy and Cesare Tinelli}, editor = {Orna Grumberg and Michael Huth}, title = {Combined Satisfiability Modulo Parametric Theories}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, {TACAS} 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4424}, pages = {602--617}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-71209-1\_47}, doi = {10.1007/978-3-540-71209-1\_47}, timestamp = {Mon, 11 Sep 2023 15:43:49 +0200}, biburl = {https://dblp.org/rec/conf/tacas/KrsticGGT07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/expert/BeckertHHSGRTBR06, author = {Bernhard Beckert and Tony Hoare and Reiner H{\"{a}}hnle and Douglas R. Smith and Cordell Green and Silvio Ranise and Cesare Tinelli and Thomas Ball and Sriram K. Rajamani}, title = {Intelligent Systems and Formal Methods in Software Engineering}, journal = {{IEEE} Intell. Syst.}, volume = {21}, number = {6}, pages = {71--81}, year = {2006}, url = {https://doi.org/10.1109/MIS.2006.117}, doi = {10.1109/MIS.2006.117}, timestamp = {Tue, 09 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/expert/BeckertHHSGRTBR06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iandc/BaaderGT06, author = {Franz Baader and Silvio Ghilardi and Cesare Tinelli}, title = {A new combination procedure for the word problem that generalizes fusion decidability results in modal logics}, journal = {Inf. Comput.}, volume = {204}, number = {10}, pages = {1413--1452}, year = {2006}, url = {https://doi.org/10.1016/j.ic.2005.05.009}, doi = {10.1016/J.IC.2005.05.009}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/BaaderGT06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/ijait/BaumgartnerFT06, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, title = {Implementing the Model Evolution Calculus}, journal = {Int. J. Artif. Intell. Tools}, volume = {15}, number = {1}, pages = {21--52}, year = {2006}, url = {https://doi.org/10.1142/S0218213006002552}, doi = {10.1142/S0218213006002552}, timestamp = {Tue, 12 May 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/ijait/BaumgartnerFT06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jacm/NieuwenhuisOT06, author = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, title = {Solving {SAT} and {SAT} Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(\emph{T})}, journal = {J. {ACM}}, volume = {53}, number = {6}, pages = {937--977}, year = {2006}, url = {https://doi.org/10.1145/1217856.1217859}, doi = {10.1145/1217856.1217859}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jacm/NieuwenhuisOT06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/BarrettNOT06, author = {Clark W. Barrett and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, editor = {Miki Hermann and Andrei Voronkov}, title = {Splitting on Demand in {SAT} Modulo Theories}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4246}, pages = {512--526}, publisher = {Springer}, year = {2006}, url = {https://doi.org/10.1007/11916277\_35}, doi = {10.1007/11916277\_35}, timestamp = {Mon, 24 Jun 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lpar/BarrettNOT06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/BaumgartnerFT06, author = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli}, editor = {Miki Hermann and Andrei Voronkov}, title = {Lemma Learning in the Model Evolution Calculus}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4246}, pages = {572--586}, publisher = {Springer}, year = {2006}, url = {https://doi.org/10.1007/11916277\_39}, doi = {10.1007/11916277\_39}, timestamp = {Sun, 12 Nov 2017 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lpar/BaumgartnerFT06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/BarrettST07, author = {Clark W. Barrett and Igor Shikanian and Cesare Tinelli}, editor = {Michael W. Mislove}, title = {An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types}, booktitle = {Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning {(PDPAR} 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), Parts of FloC 2006, Seattle, WA, USA, August 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {8}, pages = {23--37}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2006.11.037}, doi = {10.1016/J.ENTCS.2006.11.037}, timestamp = {Fri, 27 Jan 2023 14:04:30 +0100}, biburl = {https://dblp.org/rec/journals/entcs/BarrettST07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/TinelliZ05, author = {Cesare Tinelli and Calogero G. Zarba}, title = {Combining Nonstably Infinite Theories}, journal = {J. Autom. Reason.}, volume = {34}, number = {3}, pages = {209--238}, year = {2005}, url = {https://doi.org/10.1007/s10817-005-5204-9}, doi = {10.1007/S10817-005-5204-9}, timestamp = {Wed, 02 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/TinelliZ05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BaumgartnerT05, author = {Peter Baumgartner and Cesare Tinelli}, editor = {Robert Nieuwenhuis}, title = {The Model Evolution Calculus with Equality}, booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3632}, pages = {392--408}, publisher = {Springer}, year = {2005}, url = {https://doi.org/10.1007/11532231\_29}, doi = {10.1007/11532231\_29}, timestamp = {Sun, 02 Oct 2022 15:55:55 +0200}, biburl = {https://dblp.org/rec/conf/cade/BaumgartnerT05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/smt/2004, editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli}, title = {Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and the Second International Workshop on Pragmatics of Decision Procedures, PDPAR@IJCAR 2004, Cork, Ireland, July 2004}, series = {Electronic Notes in Theoretical Computer Science}, volume = {125}, number = {3}, publisher = {Elsevier}, year = {2005}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/125/issue/3}, timestamp = {Tue, 13 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/smt/2004.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BaaderGT04, author = {Franz Baader and Silvio Ghilardi and Cesare Tinelli}, editor = {David A. Basin and Micha{\"{e}}l Rusinowitch}, title = {A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics}, booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR} 2004, Cork, Ireland, July 4-8, 2004, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3097}, pages = {183--197}, publisher = {Springer}, year = {2004}, url = {https://doi.org/10.1007/978-3-540-25984-8\_11}, doi = {10.1007/978-3-540-25984-8\_11}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/BaaderGT04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cav/GanzingerHNOT04, author = {Harald Ganzinger and George Hagen and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, editor = {Rajeev Alur and Doron A. Peled}, title = {{DPLL(} {T):} Fast Decision Procedures}, booktitle = {Computer Aided Verification, 16th International Conference, {CAV} 2004, Boston, MA, USA, July 13-17, 2004, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3114}, pages = {175--188}, publisher = {Springer}, year = {2004}, url = {https://doi.org/10.1007/978-3-540-27813-9\_14}, doi = {10.1007/978-3-540-27813-9\_14}, timestamp = {Tue, 14 May 2019 10:00:43 +0200}, biburl = {https://dblp.org/rec/conf/cav/GanzingerHNOT04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/jelia/TinelliZ04, author = {Cesare Tinelli and Calogero G. Zarba}, editor = {Jos{\'{e}} J{\'{u}}lio Alferes and Jo{\~{a}}o Alexandre Leite}, title = {Combining Decision Procedures for Sorted Theories}, booktitle = {Logics in Artificial Intelligence, 9th European Conference, {JELIA} 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3229}, pages = {641--653}, publisher = {Springer}, year = {2004}, url = {https://doi.org/10.1007/978-3-540-30227-8\_53}, doi = {10.1007/978-3-540-30227-8\_53}, timestamp = {Tue, 07 May 2024 20:11:09 +0200}, biburl = {https://dblp.org/rec/conf/jelia/TinelliZ04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lpar/NieuwenhuisOT04, author = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, editor = {Franz Baader and Andrei Voronkov}, title = {Abstract {DPLL} and Abstract {DPLL} Modulo Theories}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, {LPAR} 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3452}, pages = {36--50}, publisher = {Springer}, year = {2004}, url = {https://doi.org/10.1007/978-3-540-32275-7\_3}, doi = {10.1007/978-3-540-32275-7\_3}, timestamp = {Tue, 14 May 2019 10:00:55 +0200}, biburl = {https://dblp.org/rec/conf/lpar/NieuwenhuisOT04.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/AhrendtBNRT05, author = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli}, editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli}, title = {Preface}, booktitle = {Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and the Second International Workshop on Pragmatics of Decision Procedures, PDPAR@IJCAR 2004, Cork, Ireland, July 2004}, series = {Electronic Notes in Theoretical Computer Science}, volume = {125}, number = {3}, pages = {1--2}, publisher = {Elsevier}, year = {2004}, url = {https://doi.org/10.1016/j.entcs.2005.02.025}, doi = {10.1016/J.ENTCS.2005.02.025}, timestamp = {Tue, 13 Dec 2022 13:53:40 +0100}, biburl = {https://dblp.org/rec/journals/entcs/AhrendtBNRT05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/Tinelli03, author = {Cesare Tinelli}, title = {Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing}, journal = {J. Autom. Reason.}, volume = {30}, number = {1}, pages = {1--31}, year = {2003}, url = {https://doi.org/10.1023/A:1022587501759}, doi = {10.1023/A:1022587501759}, timestamp = {Wed, 02 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/Tinelli03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tcs/TinelliR03, author = {Cesare Tinelli and Christophe Ringeissen}, title = {Unions of non-disjoint theories and combinations of satisfiability procedures}, journal = {Theor. Comput. Sci.}, volume = {290}, number = {1}, pages = {291--353}, year = {2003}, url = {https://doi.org/10.1016/S0304-3975(01)00332-2}, doi = {10.1016/S0304-3975(01)00332-2}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tcs/TinelliR03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tcs/TinelliR03a, author = {Cesare Tinelli and Teodor Rus}, title = {Preface}, journal = {Theor. Comput. Sci.}, volume = {291}, number = {3}, pages = {219--221}, year = {2003}, url = {https://doi.org/10.1016/S0304-3975(02)00363-8}, doi = {10.1016/S0304-3975(02)00363-8}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tcs/TinelliR03a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BaumgartnerT03, author = {Peter Baumgartner and Cesare Tinelli}, editor = {Franz Baader}, title = {The Model Evolution Calculus}, booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2741}, pages = {350--364}, publisher = {Springer}, year = {2003}, url = {https://doi.org/10.1007/978-3-540-45085-6\_32}, doi = {10.1007/978-3-540-45085-6\_32}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/BaumgartnerT03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/TinelliZ03, author = {Cesare Tinelli and Calogero G. Zarba}, editor = {Ingo Dahn and Laurent Vigneron}, title = {Combining Non-Stably Infinite Theories}, booktitle = {4th International Workshop on First-Order Theorem Proving, {FTP} 2003, in connection with {RDP} 2003, Federated Conference on Rewriting, Deduction and Programming, Valencia, Spain, June 12-14, 2003}, series = {Electronic Notes in Theoretical Computer Science}, volume = {86}, number = {1}, pages = {35--48}, publisher = {Elsevier}, year = {2003}, url = {https://doi.org/10.1016/S1571-0661(04)80651-0}, doi = {10.1016/S1571-0661(04)80651-0}, timestamp = {Thu, 08 Dec 2022 13:39:47 +0100}, biburl = {https://dblp.org/rec/journals/entcs/TinelliZ03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iandc/BaaderT02, author = {Franz Baader and Cesare Tinelli}, title = {Deciding the Word Problem in the Union of Equational Theories}, journal = {Inf. Comput.}, volume = {178}, number = {2}, pages = {346--390}, year = {2002}, url = {https://doi.org/10.1006/inco.2001.3118}, doi = {10.1006/INCO.2001.3118}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/BaaderT02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/jelia/Tinelli02, author = {Cesare Tinelli}, editor = {Sergio Flesca and Sergio Greco and Nicola Leone and Giovambattista Ianni}, title = {A DPLL-Based Calculus for Ground Satisfiability Modulo Theories}, booktitle = {Logics in Artificial Intelligence, European Conference, {JELIA} 2002, Cosenza, Italy, September, 23-26, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2424}, pages = {308--319}, publisher = {Springer}, year = {2002}, url = {https://doi.org/10.1007/3-540-45757-7\_26}, doi = {10.1007/3-540-45757-7\_26}, timestamp = {Tue, 14 May 2019 10:00:44 +0200}, biburl = {https://dblp.org/rec/conf/jelia/Tinelli02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/BaaderT02, author = {Franz Baader and Cesare Tinelli}, editor = {Sophie Tison}, title = {Combining Decision Procedures for Positive Theories Sharing Constructors}, booktitle = {Rewriting Techniques and Applications, 13th International Conference, {RTA} 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2378}, pages = {352--366}, publisher = {Springer}, year = {2002}, url = {https://doi.org/10.1007/3-540-45610-4\_25}, doi = {10.1007/3-540-45610-4\_25}, timestamp = {Tue, 14 May 2019 10:00:46 +0200}, biburl = {https://dblp.org/rec/conf/rta/BaaderT02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/frocos/BaaderT00, author = {Franz Baader and Cesare Tinelli}, editor = {H{\'{e}}l{\`{e}}ne Kirchner and Christophe Ringeissen}, title = {Combining Equational Theories Sharing Non-Collapse-Free Constructors}, booktitle = {Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1794}, pages = {260--274}, publisher = {Springer}, year = {2000}, url = {https://doi.org/10.1007/10720084\_17}, doi = {10.1007/10720084\_17}, timestamp = {Tue, 14 May 2019 10:00:51 +0200}, biburl = {https://dblp.org/rec/conf/frocos/BaaderT00.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@phdthesis{DBLP:phd/us/Tinelli99, author = {Cesare Tinelli}, title = {Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning}, school = {University of Illinois Urbana-Champaign, {USA}}, year = {1999}, url = {https://hdl.handle.net/2142/81950}, timestamp = {Thu, 14 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/phd/us/Tinelli99.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/BaaderT99, author = {Franz Baader and Cesare Tinelli}, editor = {Paliath Narendran and Micha{\"{e}}l Rusinowitch}, title = {Deciding the Word Problem in the Union of Equational Theories Sharing Constructors}, booktitle = {Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1631}, pages = {175--189}, publisher = {Springer}, year = {1999}, url = {https://doi.org/10.1007/3-540-48685-2\_14}, doi = {10.1007/3-540-48685-2\_14}, timestamp = {Tue, 14 May 2019 10:00:46 +0200}, biburl = {https://dblp.org/rec/conf/rta/BaaderT99.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jflp/TinelliH98, author = {Cesare Tinelli and Mehdi T. Harandi}, title = {Constraint Logic Programming over Unions of Constraint Theories}, journal = {J. Funct. Log. Program.}, volume = {1998}, number = {6}, year = {1998}, url = {http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-06/A98-06.html}, timestamp = {Wed, 01 Apr 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jflp/TinelliH98.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/BaaderT97, author = {Franz Baader and Cesare Tinelli}, editor = {William McCune}, title = {A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method}, booktitle = {Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1249}, pages = {19--33}, publisher = {Springer}, year = {1997}, url = {https://doi.org/10.1007/3-540-63104-6\_3}, doi = {10.1007/3-540-63104-6\_3}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/BaaderT97.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cp/TinelliH96, author = {Cesare Tinelli and Mehdi T. Harandi}, editor = {Eugene C. Freuder}, title = {Constraint Logic Programming over Unions of Constraint Theories}, booktitle = {Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, Cambridge, Massachusetts, USA, August 19-22, 1996}, series = {Lecture Notes in Computer Science}, volume = {1118}, pages = {436--450}, publisher = {Springer}, year = {1996}, url = {https://doi.org/10.1007/3-540-61551-2\_92}, doi = {10.1007/3-540-61551-2\_92}, timestamp = {Tue, 14 May 2019 10:00:45 +0200}, biburl = {https://dblp.org/rec/conf/cp/TinelliH96.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/frocos/TinelliH96, author = {Cesare Tinelli and Mehdi T. Harandi}, editor = {Franz Baader and Klaus U. Schulz}, title = {A New Correctness Proof of the \{Nelson-Oppen\} Combination Procedure}, booktitle = {Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26-29, 1996, Proceedings}, series = {Applied Logic Series}, volume = {3}, pages = {103--119}, publisher = {Kluwer Academic Publishers}, year = {1996}, timestamp = {Mon, 20 Mar 2017 13:54:49 +0100}, biburl = {https://dblp.org/rec/conf/frocos/TinelliH96.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icsm/AvellisIPST91, author = {Gianna Avellis and Andrea Iacobbe and Dario Palmisano and Giovanni Semeraro and Cesare Tinelli}, title = {An analysis of incremental assistant capabilities of a software evolution expert system}, booktitle = {Proceedings of the Conference on Software Maintenance, {ICSM} 1991, Sorrento, Italy, 15-17 October 1991}, pages = {220--227}, publisher = {{IEEE}}, year = {1991}, url = {https://doi.org/10.1109/ICSM.1991.160334}, doi = {10.1109/ICSM.1991.160334}, timestamp = {Tue, 31 Oct 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/icsm/AvellisIPST91.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.