Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

5 résultats
Image document

Certified proofs in programs involving exceptions

Jean-Guillaume Dumas , Dominique Duval , Burak Ekici , Jean-Claude Reynaud
Conference on Intelligent Computer Mathematics Work in Progress, Jul 2014, Coimbra, Portugal. pp.16
Communication dans un congrès hal-00867237v3
Image document

SMTCoq: A plug-in for integrating SMT solvers into Coq

Burak Ekici , Alain Mebsout , Cesare Tinelli , Chantal Keller , Guy Katz , et al.
Computer Aided Verification - 29th International Conference, Jul 2017, Heidelberg, Germany
Communication dans un congrès hal-01669345v1
Image document

IMP with exceptions over decorated logic

Burak Ekici
Discrete Mathematics and Theoretical Computer Science, 2018, vol. 20 no. 2, ⟨10.23638/DMTCS-20-2-11⟩
Article dans une revue hal-01132831v9
Image document

Hilbert-Post completeness for the state and the exception effects

Jean-Guillaume Dumas , Dominique Duval , Burak Ekici , Jean-Claude Reynaud , Damien Pous
Sixth International Conference on Mathematical Aspects of Computer and Information Sciences, Nov 2015, Berlin, Germany. pp.596-610, ⟨10.1007/978-3-319-32859-1_51⟩
Communication dans un congrès hal-01121924v3
Image document

Formal verification in Coq of program properties involving the global state effect

Jean-Guillaume Dumas , Dominique Duval , Burak Ekici , Damien Pous
JFLA 2014 - Journées Francophones des Langages Applicatifs, Jan 2014, Fréjus, France. pp.1-17
Communication dans un congrès hal-00869230v2