Burak Ekici
previous employment
email: burak.ekici@tedu.edu.tr
office: Department of Computer Engineering, TED University, Ankara.
Publications
 Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq
B. Ekici and C. Kaliszyk at Mathematics in Computer Science, February 2020.
 Verifying Bitvector Invertibility Conditions in Coq
B. Ekici, A. Viswanathan, Y. Zohar, C. Barrett and C. Tinelli at PxTP 2019.
 IMP with exceptions over decorated logic
B. Ekici at Discrete Mathematics and Theoretical Computer Science, vol. 20, no. 2, October 2018.
 Concrete Semantics with Coq and CoqHammer
Ł. Czajka, B. Ekici and C. Kaliszyk at CICM 2018.

Towards Mac Lane’s Comparison Theorem for the Kleisli construction in Coq
B. Ekici at FMM in CICM 2018.

SMTCoq: A plugin for integrating SMT solvers into Coq
B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds and C. Barrett at CAV 2017.

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
B. Ekici, G. Katz, C. Keller, A. Mebsout, A. Reynolds and C. Tinelli at HaTT 2016.

HilbertPost completeness for the state and the exception effects
J.G. Dumas, D. Duval, B. Ekici, D. Pous and J.C. Reynaud at MACIS 2015.

Certified proofs in programs involving exceptions
J.G. Dumas, D. Duval, B. Ekici and J.C. Reynaud at CICM 2014 (work in progress).

Formal verification in Coq of program properties involving the global state effect
J.G. Dumas, D. Duval, B. Ekici and D. Pous at JFLA 2014.
PhD thesis
Teaching
 Main Course: Theory of Computation (20202021)
 Main Course: Digital Design (20192020)
 Main Course: Microprocessors (20192020)
 Main Course: Programming Languages (20192020)
 Proseminar:
Discrete Mathematics (20182019)
Software development
Recent Talks
CV