I am a Phd student at Inria Nancy in the VeriDis team and I’m part of the Matryoshka project. The main goal of my Phd is to design an higher-order SMT-solver. My supervisors are Pascal Fontaine and Jasmin Christian Blanchette. I’m graduated of MSc degree in Computer Sciences from (MPRI) at University of Paris Diderot in 2017.

---

Publications and projects

Machine learning for instance selection in SMT solving (Full paper)

Daniel El Ouraoui, Pascal Fontaine, and Cezary Kaliszyk. Preprint (PDF)

Extending SMT solvers to higher-order logic

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 35–54, Springer, 2019. Preprint (PDF) Report (PDF)

Machine learning for instance selection in SMT solving

Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine, and Cezary Kaliszyk. In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019). Preprint (PDF)

Higher-order SMT solving (work in progress)

Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. In Dimitrova, R., D’Silva, V. (eds.), 16th International Workshop on Satisfiability Modulo Theories (SMT 2018). Preprint (PDF)

Language and proofs for higher-order SMT (work in progress)

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. Accepted at 5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017). Preprint (PDF)

Proof in Coq of the IE property for the Linear Substitution (Ls)

Code here
This is a formalization of the proof of Beniamino Accattoli of the preservation of the strong normalization of linear substitution realized in L3 and M1 internships, at the LIPN. My advisors were Micaela Mayero and Damiano Mazza. For more details you may look in the unpublished article about this formalization here