Personnel

 BURAK EKİCİ
Burak Ekici
@ E-mail
burakekici@mu.edu.tr
Phone

Staff of

Place of Duty

Mühendislik Fakültesi / Bilgisayar Mühendisliği Bölümü / Bilgisayar Donanımı Abd

Regular Staff

Mühendislik Fakültesi / Bilgisayar Mühendisliği Bölümü / Bilgisayar Donanımı Abd

Education

Bachelor's Degree

İzmir Institute of Technology - Faculty of Engineering - Computer Engineering - 2009

Master's Degree

Yaşar University - Faculty of Engineering - Computer Engineering - 2012

Doctorate

(Post-doktora) - University of Oxford - Department of Computer Science - Formal Logic - 2023 - Devam Ediyor
(Doktora) - Université Grenoble Alpes - ED MSTII - Mathematics and Informatics - 2015
(Post-doktora) - University of Iowa - Department of Computer Science - Informatics - 2017
(Post-doktora) - University of Innsbruck - Department of Computer Science - Computational Logic - 2019

Academic Publishing

(A-1) Articles published in journals indexed by SCI or SCI Expanded, SSCI, AHCI

1-) Ekici Burak, 2023. A Sound Definitional Interpreter for a Simply Typed Functional Language. Axioms
2-) Ekici Burak, 2022. Formal categorical reasoning. Turkish Journal of Mathematics
3-) Ekici Burak, 2018. IMP with exceptions over decorated logic. Discrete Mathematics and Theoretical Computer Science

(A-3)

1-) Ekici Burak, Kaliszyk Cezary, 2020. Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq. Mathematics in Computer Science

(B-1) Papers verbally presented or published in scientific and art meetings like international conferences, symposiums, panels, and workshops

1-) Ekici Burak, Viswanathan Arjun, Zohar Yoni, Tinelli Cesare, Barrett Clark, 2023. Formal Verification of Bit-vector Invertibility Conditions in Coq. The 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023)
2-) Ekici Burak, Viswanathan Arjun, Zohar Yoni, Tinelli Cesare, Barrett Clark, 2019. Verifying Bit-vector Invertibility Conditions in Coq. Sixth Workshop on Proof eXchange for Theorem Proving (PxTP 2019 in CADE-27)
3-) Ekici Burak, 2018. Towards Mac Lane’s Comparison Theorem for the (co)Kleisli Construction in Coq. Third workshop on Formal Mathematics for Mathematicians (FMM in CICM 2018)
4-) Czajka Lukasz, Ekici Burak, Kaliszyk Cezary, 2018. Concrete Semantics with Coq and CoqHammer. 11th Conference on Intelligent Computer Mathematics (CICM 2018)
5-) Ekici Burak, Tinelli Cesare, Katz Guy, Keller Chantal, Mebsout Alain, Reynolds Anrdew, Reynolds Anrdew, 2017. SMTCoq: A plug-in for integrating SMT solvers into Coq. Computer Aided Verification, 29th International Conference
6-) Ekici Burak, Reynolds Anrdew, Tinelli Cesare, Katz Guy, Keller Chantal, Mebsout Alain, 2016. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). HaTT 2016: Hammers for Type Theories
7-) Ekici Burak, Dumas Jean-guillaume, Duval Dominique, Pous Damien, Reynaud Jean-claude, 2015. Hilbert-Post completeness for the state and the exception effects. International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2015)
8-) Ekici Burak, Duval Dominique, Dumas Jean-guillaume, Reynaud Jean-claude, 2014. Certified proofs in programs involving exceptions. Conference on Intelligent Computer Mathematics (CICM) 2014
9-) Ekici Burak, Dumas Jean-guillaume, Duval Dominique, Pous Damien, 2014. Formal verification in Coq of program properties involving the global state effect. JFLA 2014 - Journées Francophones des Langages Applicatifs

(B-2)

1-) Ekici Burak, 2022. Formal Categorical Reasoning. Studies on Scientific Developments in Geometry, Algebra, and Applied Mathematics
2-) Ekici Burak, 2019. Univalent Typoids in Coq. TYPES in Munich

(B-3)

1-) Ekici Burak, 2015. Relative Hilbert-Post completeness for exceptions. Fundations Seminar

(B-4) Papers verbally presented or published in scientific and art meetings like national conferences, symposiums, panels, and workshops

1-) Yücel Çağatay, Koltuksuz Ahmet Hasan, Kılınç Görkem, Ekici Burak, 2010. Kategori Kuramının Bilgisayar Bilimleri Ve Yazılım Mühendisliği Alanındaki Uygulamaları. 9. Matematik Sempozyumu

(E-1)

1-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2022 Atıf Sayısı: 1
2-) Verifying Bit-vector Invertibility Conditions in Coq - Atıf Yılı: 2021 Atıf Sayısı: 2
3-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2021 Atıf Sayısı: 2
4-) Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) - Atıf Yılı: 2020 Atıf Sayısı: 1
5-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2020 Atıf Sayısı: 1
6-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2019 Atıf Sayısı: 1
7-) Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) - Atıf Yılı: 2019 Atıf Sayısı: 1
8-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2018 Atıf Sayısı: 1
9-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2017 Atıf Sayısı: 1

(E-2)

1-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2022 Atıf Sayısı: 1
2-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2021 Atıf Sayısı: 1
3-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2019 Atıf Sayısı: 1

(E-6)

1-) SMTCoq: A plug-in for integrating SMT solvers into Coq - Atıf Yılı: 2019 Atıf Sayısı: 1
2-) Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) - Atıf Yılı: 2019 Atıf Sayısı: 1

(G-2) Being part of a project supported by international institutions (researcher, trainer, advisor, etc.)

1-) Proje Durum: Tamamlandı. Projedeki Görev: Araştırmacı. Konu: . Proje Türü: Avrupa Birliği. ERC Project "SMART" Starting Grant no. 714034. 2017-2022
2-) Proje Durum: Tamamlandı. Projedeki Görev: Araştırmacı. Konu: Cetifying CVC4 generated proofs employing SMTCoq plug-in. Proje Türü: Diğer(Uluslararası). CERTIFIED SATISFIABILITY MODULO THEORIES (SMT) SOLVING FOR SYSTEM VERIFICATION. 2013-2017

Courses

CENG 2010 2022-2023 Bahar

Programming Language Concepts

CENG 2034 2022-2023 Bahar

Operating Systems

CENG 4005 2022-2023 Bahar

Formal Languages and Abstract Machines

CENG 4011 2022-2023 Bahar

Senior Design Project I

CENG 4012 2022-2023 Bahar

Senior Design Project II

CENG 3549 2022-2023 Güz

Functional Programming

CENG 4005 2022-2023 Güz

Formal Languages and Abstract Machines