| SMTCoq: A plug-in for integrating SMT solvers into Coq B Ekici, A Mebsout, C Tinelli, C Keller, G Katz, A Reynolds, C Barrett Computer Aided Verification: 29th International Conference, CAV 2017 …, 2017 | 118 | 2017 |
| Extending SMTCoq, a certified checker for SMT B Ekici, G Katz, C Keller, A Mebsout, AJ Reynolds, C Tinelli arXiv preprint arXiv:1606.05947, 2016 | 18 | 2016 |
| Formal verification in Coq of program properties involving the global state effect JG Dumas, D Duval, B Ekici, D Pous arXiv preprint arXiv:1310.0794, 2013 | 12 | 2013 |
| Certified proofs in programs involving exceptions JG Dumas, D Duval, B Ekici, JC Reynaud arXiv preprint arXiv:1310.2338, 2013 | 8 | 2013 |
| Procedural and Non-Procedural Implementation of Search Strategies in Control Network Programming K Kratchanov, E Golemanova, T Golemanov, T Ercan, B Ekici arXiv preprint arXiv:1412.4184, 2014 | 5 | 2014 |
| Concrete semantics with Coq and CoqHammer Ł Czajka, B Ekici, C Kaliszyk Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018 | 4 | 2018 |
| Relative hilbert-post completeness for exceptions JG Dumas, D Duval, B Ekici, D Pous, JC Reynaud Mathematical Aspects of Computer and Information Sciences: 6th International …, 2016 | 4 | 2016 |
| Certified proofs in programs involving exceptions. CICM 2014 JG Dumas, D Duval, B Ekici, JC Reynaud CEUR Workshop Proceedings 1186, 2014 | 4 | 2014 |
| Verifying bit-vector invertibility conditions in coq B Ekici, A Viswanathan, Y Zohar, C Barrett, C Tinelli arXiv preprint arXiv:1908.09478, 2019 | 3 | 2019 |
| IMP with exceptions over decorated logic B Ekici Discrete Mathematics & Theoretical Computer Science 20 (Automata, Logic and …, 2018 | 2 | 2018 |
| Certification de programmes avec des effets calculatoires B Ekici, JG Dumas, D Duval, D Pous PhD thesis, 2015. URL https://tel. archives-ouvertes. fr/tel-01250842/document, 2015 | 2 | 2015 |
| Completeness of Asynchronous Session Tree Subtyping in Coq B Ekici, N Yoshida 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 | 1 | 2024 |
| Formal Verification of Bit-Vector Invertibility Conditions in Coq B Ekici, A Viswanathan, Y Zohar, C Tinelli, C Barrett International Symposium on Frontiers of Combining Systems, 41-59, 2023 | 1 | 2023 |
| Formal categorical reasoning B Ekici Turkish Journal of Mathematics 46 (4), 1538-1552, 2022 | 1 | 2022 |
| Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq B Ekici, C Kaliszyk Mathematics in Computer Science 14, 533-549, 2020 | 1 | 2020 |
| Towards Mac Lane's Comparison Theorem for the (co) Kleisli Construction in Coq. B Ekici CICM Workshops, 2018 | 1 | 2018 |
| Certification of programs with computational effects B Ekici Université Grenoble Alpes, 2015 | 1 | 2015 |
| A Sound Definitional Interpreter for a Simply Typed Functional Language B Ekici Axioms 12 (1), 43, 2022 | | 2022 |
| Verifying Bit-vector Invertibility Conditions in Coq–Extended Abstract B Ekici, A Viswanathan, Y Zohar, C Barrett, C Tinelli | | |
Cesare TinelliProfessor of Computer Science, The University of IowaVerified email at uiowa.edu
