{"id":13,"date":"2015-06-15T10:26:53","date_gmt":"2015-06-15T08:26:53","guid":{"rendered":"http:\/\/members.loria.fr\/thierrygartiser\/?page_id=13"},"modified":"2021-03-08T01:28:21","modified_gmt":"2021-03-07T23:28:21","slug":"publications","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/SStratulat\/publications\/","title":{"rendered":"Publications"},"content":{"rendered":"<ul>\n<li>\n<h4><a href=\"http:\/\/dblp.uni-trier.de\/pers\/hd\/s\/Stratulat:Sorin\">DBLP<\/a><\/h4>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<hr \/>\n<h1>Publications depuis 2010<\/h1>\n<p>&nbsp;<\/p>\n<p>   <!DOCTYPE html PUBLIC \"-\/\/W3C\/\/DTD XHTML 1.0 Transitional\/\/EN\" \"http:\/\/www.w3.org\/TR\/xhtml1\/DTD\/xhtml1-transitional.dtd\"> <html xmlns='http:\/\/www.w3.org\/1999\/xhtml' xml:lang='fr' lang='fr'> <head> <meta name=\"robots\" content=\"noindex, nofollow\" \/> <meta http-equiv=\"content-type\" content= \"text\/html;charset=UTF-8\" \/> <meta http-equiv=\"Content-Language\" content=\"fr\" \/> <link rel=\"stylesheet\" type=\"text\/css\" href=\"..\/css\/VisuGen.css\" \/> <link rel=\"stylesheet\" type=\"text\/css\" href=\"https:\/\/haltools.inria.fr\/\/css\/VisuRubriqueEncadre.css\" \/> <!-- Piwik haltools.inria.fr--> <script type=\"text\/javascript\">   var _paq = _paq || [];   _paq.push(['trackPageView']);   _paq.push(['enableLinkTracking']);   (function() {     var u=\"\/\/piwik.inria.fr\/\";     _paq.push(['setTrackerUrl', u+'piwik.php']);     _paq.push(['setSiteId', 25]);     var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];     g.type='text\/javascript'; g.async=true; g.defer=true; g.src=u+'piwik.js'; s.parentNode.insertBefore(g,s);   })(); <\/script> <noscript><\/p>\n<p><img decoding=\"async\" src=\"\/\/piwik.inria.fr\/piwik.php?idsite=25\" style=\"border:0;\" alt=\"\" \/><\/p>\n<p><\/noscript> <!-- End Piwik Code -->  <title>Publications HAL de  Sorin, Stratulat<\/title> <\/head> <body> <\/p>\n<div id=\"res_script\">\n<p class='Rubrique'>2025<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-05447018v1\" target=\"_blank\" >AIROBO: A EUROPEAN PROJECT FOR SOFTWARE ENGINEERS<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">I Dramnesc, E Abraham, N Fachantidis, T Jebelean, G Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>EDULEARN 2025 &#8211; 17th International Conference on Education and New Learning Technologies<\/i>, Jun 2025, Palma De Majorque, Spain. pp.1221-1228, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.21125\/edulearn.2025.0394\">&#x27E8;10.21125\/edulearn.2025.0394&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-05447018\/file\/EDULEARN25_394_proceedings_v1.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-05447018\/file\/EDULEARN25_394_proceedings_v1.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-05447018\/file\/EDULEARN25_394_proceedings_v1.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-05447018v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-05447056v1\" target=\"_blank\" >AiRobo: A EU Project on Artificial Intelligence and Robotics for Higher Education<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Erika Abraham, Nikolaos Fachantidis, Tudor Jebelean, Gabor Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>ED-MEDIA 2025 &#8211; EdMedia + Innovate Learning<\/i>, May 2025, Barcelona, Spain. pp.1198-1203<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-05447056\/file\/EdMedia_proceedings.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-05447056\/file\/EdMedia_proceedings.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-05447056\/file\/EdMedia_proceedings.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-05447056v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2024<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-04814646v2\" target=\"_blank\" >A European Project on AI-based Robotics<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Erika \u00c1brah\u00e1m, Tudor Jebelean, Nikolaos Fachantidis, G\u00e1bor Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>TALE2024 (International Conference on Teaching, Assessment and Learning for Engineering)<\/i>, Dec 2024, Bengalore, India<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-04814646\/file\/TALE_2024___paper%20%281%29.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-04814646\/file\/TALE_2024___paper%20%281%29.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-04814646\/file\/TALE_2024___paper%20%281%29.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-04814646v2\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-04678850v1\" target=\"_blank\" >Certification of Sorting Algorithms Using Theorema and Coq<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SCSS 2024 (Symbolic Computation in Software Science)<\/i>, Aug 2024, Tokyo (Japan), Japan. pp.38&#8211;56, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-031-69042-6_3\">&#x27E8;10.1007\/978-3-031-69042-6_3&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-04678850\/file\/paper-scss-2024.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-04678850\/file\/paper-scss-2024.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-04678850\/file\/paper-scss-2024.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-04678850v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-04608767v1\" target=\"_blank\" >Certification of Tail Recursive Bubble-Sort in Theorema and Coq<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>25th International Conference on Logic Programming and Automated Reasoning (LPAR)Complementary Volume<\/i>, May 2024, Balaclava, Mauritius. pp.53&#8211;68<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-04608767\/file\/LPAR.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-04608767\/file\/LPAR.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-04608767\/file\/LPAR.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-04608767v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2023<\/p>\n<p class='SousRubrique'>Journal articles<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-03993176v2\" target=\"_blank\" >Mechanical certification of FOLID cyclic proofs<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Annals of Mathematics and Artificial Intelligence<\/i>, 2023, 95 (5), pp.651-673. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/s10472-023-09832-7\">&#x27E8;10.1007\/s10472-023-09832-7&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-03993176\/file\/amai2022.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-03993176\/file\/amai2022.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-03993176\/file\/amai2022.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-03993176v2\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2022<\/p>\n<p class='SousRubrique'>Journal articles<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-03886685v1\" target=\"_blank\" >Automated Reasoning in the Class<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Erika \u00c1brah\u00e1m, Tudor Jebelean, G\u00e1bor Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Computer-Algebra-Rundbrief<\/i>, 2022, 71, pp.21-26<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-03886685\/file\/paper.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-03886685\/file\/paper.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-03886685\/file\/paper.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-03886685v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-03688845v2\" target=\"_blank\" >R\u00e9currence noeth\u00e9rienne pour le raisonnement de premier ordre<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>1024 : Bulletin de la Soci\u00e9t\u00e9 Informatique de France<\/i>, 2022, 19, pp.157-169. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.48556\/SIF.1024.19.157\">&#x27E8;10.48556\/SIF.1024.19.157&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-03688845\/file\/Str__2022a.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-03688845\/file\/Str__2022a.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-03688845\/file\/Str__2022a.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-03688845v2\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-03781994v1\" target=\"_blank\" >Experiments with\u00a0Automated Reasoning in\u00a0the\u00a0Class<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Erika \u00c1brah\u00e1m, Tudor Jebelean, G\u00e1bor Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>CICM 2022 &#8211; 15th Conference on Intelligent Computer Mathematics<\/i>, Sep 2022, Tbilisi \/ Hybrid, Georgia. pp.287-304, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-031-16681-5_20\">&#x27E8;10.1007\/978-3-031-16681-5_20&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-03781994\/file\/paper.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-03781994\/file\/paper.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-03781994\/file\/paper.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-03781994v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-03900003v1\" target=\"_blank\" >ARC: An Educational Project on Automated Reasoning in the Class<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dr\u0103mnesc, Tudor Jebelean, Erika \u00c1brah\u00e1m, G\u00e1bor Kusper, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>EdMedia + Innovate Learning 2022 &#8211; AACE Conferences<\/i>, Jun 2022, New York, United States<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-03900003\/file\/I.%20__2022.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-03900003\/file\/I.%20__2022.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-03900003\/file\/I.%20__2022.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-03900003v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2021<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-02464242v4\" target=\"_blank\" >E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SCSS 2021 &#8211; 9th International Symposium on Symbolic Computation in Software Science<\/i>, Sep 2021, Linz, Austria. pp.129&#8211;135<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-02464242\/file\/SCSS2021.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-02464242\/file\/SCSS2021.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-02464242\/file\/SCSS2021.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-02464242v4\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>Habilitation \u00e0 diriger des recherches<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/tel-03286314v1\" target=\"_blank\" >Noetherian Induction for Computer-Assisted First-Order Reasoning<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\">Symbolic Computation [cs.SC]. Universit\u00e9 de Lorraine, 2021<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/tel-03286314\/file\/main.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/tel-03286314\/file\/main.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/tel-03286314\/file\/main.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/tel-03286314v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2020<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-02965319v2\" target=\"_blank\" >SPIKE, an automatic theorem prover &#8212; revisited<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SYNASC2020 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing<\/i>, Sep 2020, Timisoara, Romania. pp.93-96<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-02965319\/file\/synasc2020.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-02965319\/file\/synasc2020.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-02965319\/file\/synasc2020.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-02965319v2\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2019<\/p>\n<p class='SousRubrique'>Journal articles<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590654v1\" target=\"_blank\" >Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Journal of Symbolic Computation<\/i>, 2019, 90, pp.3-41. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.jsc.2018.04.002\">&#x27E8;10.1016\/j.jsc.2018.04.002&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590654\/file\/paper.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590654\/file\/paper.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590654\/file\/paper.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590654v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>Other publications<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-02398634v1\" target=\"_blank\" >Efficient Validation of FOL ID Cyclic Induction Reasoning<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\">2019<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-02398634\/file\/CiSS2019.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-02398634\/file\/CiSS2019.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-02398634\/file\/CiSS2019.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-02398634v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2018<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01883826v1\" target=\"_blank\" >Validating Back-links of FOLID Cyclic Pre-proofs<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>CL&#038;C&rsquo;18 &#8211; Seventh International Workshop on Classical Logic and Computation<\/i>, Jul 2018, Oxford, United Kingdom. pp.39&#8211;53<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01883826\/file\/Str__2018.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01883826\/file\/Str__2018.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01883826\/file\/Str__2018.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01883826v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2017<\/p>\n<p class='SousRubrique'>Journal articles<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590649v1\" target=\"_blank\" >Mechanically Certifying Formula-based Noetherian Induction Reasoning<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Journal of Symbolic Computation<\/i>, 2017, 80, Part I, pp.209-249. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1016\/j.jsc.2016.07.014\">&#x27E8;10.1016\/j.jsc.2016.07.014&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590649\/file\/Str_JSC_2016.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590649\/file\/Str_JSC_2016.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590649\/file\/Str_JSC_2016.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590649v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590651v1\" target=\"_blank\" >Cyclic Proofs with Ordering Constraints<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods)<\/i>, Sep 2017, Brasilia, Brazil. pp.311 &#8211; 327, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-66902-1_19\">&#x27E8;10.1007\/978-3-319-66902-1_19&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590651\/file\/Str_10501_2017a.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590651\/file\/Str_10501_2017a.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590651\/file\/Str_10501_2017a.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590651v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2016<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590647v1\" target=\"_blank\" >Structural vs. Cyclic Induction<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SYNASC&rsquo;2016 International Symposium on Symbolic and Numeric Algorithms for Scientific Computing<\/i>, Sep 2016, Timisoara, Romania. pp.29 &#8211; 36, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1109\/SYNASC.2016.018\">&#x27E8;10.1109\/SYNASC.2016.018&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590647\/file\/Str__2016b.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590647\/file\/Str__2016b.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590647\/file\/Str__2016b.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590647v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590637v1\" target=\"_blank\" >A Case Study on Algorithm Discovery from Proofs: The Insert Function on Binary Trees<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SACI 2016: 11th IEEE International Symposium on Applied Computational Intelligence and Informatics<\/i>, May 2016, Timisoara, Romania<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590637\/file\/DraJebStr__2016a.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590637\/file\/DraJebStr__2016a.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590637\/file\/DraJebStr__2016a.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590637v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590645v1\" target=\"_blank\" >Proof\u2013based Synthesis of Sorting Algorithms for Trees<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>140th International Conference on Language and Automata Theory and Applications (LATA 2016)<\/i>, Mar 2016, Prague, Czech Republic. pp.562-575, <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1007\/978-3-319-30000-9_43\">&#x27E8;10.1007\/978-3-319-30000-9_43&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590645\/file\/DraJebStr__2016.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590645\/file\/DraJebStr__2016.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590645\/file\/DraJebStr__2016.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590645v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2015<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01590633v1\" target=\"_blank\" >Combinatorial Techniques for Proof-Based Synthesis of Sorting Algorithms<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SYNASC 2015: 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing<\/i>, Sep 2015, Timisoara, Romania<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01590633\/file\/DraJebStr__2015a.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01590633\/file\/DraJebStr__2015a.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01590633\/file\/DraJebStr__2015a.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01590633v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01235173v1\" target=\"_blank\" >Theory Exploration of Binary Trees<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>13th IEEE International Symposium on Intelligent Systems and Informatics, SISY 2015<\/i>, Sep 2015, Subotica, Serbia. pp.139-144<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01235173\/file\/sisy2015.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01235173\/file\/sisy2015.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01235173\/file\/sisy2015.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01235173v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01235170v1\" target=\"_blank\" >Better Careers for Transnational European Students ? -a case study for French-German diploma alumni<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Gabriel Michel, V\u00e9ronique Jeanclaude, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>ICEUTE&rsquo;15: 6th International Conference on EUropean Transnational Education<\/i>, Jun 2015, Burgos, Spain<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01235170\/file\/document.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01235170\/file\/document.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01235170\/file\/document.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01235170v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2014<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01098933v1\" target=\"_blank\" >Implementing Reasoning Modules in Implicit Induction Theorem Provers<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2014)<\/i>, Sep 2014, Timisoara, Romania<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01098933\/file\/synasc2014_submission_87%20%281%29.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01098933\/file\/synasc2014_submission_87%20%281%29.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01098933\/file\/synasc2014_submission_87%20%281%29.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01098933v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-01098929v1\" target=\"_blank\" >Decision Procedures for Proving Inductive Theorems without Induction<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Takahito Aoto, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>16th International Symposium on Principles and Practice of Declarative Programming (PPDP) 2014<\/i>, Sep 2014, Canterbury, United Kingdom. <a target=\"_blank\" href=\"https:\/\/dx.doi.org\/10.1145\/2643135.2643156\">&#x27E8;10.1145\/2643135.2643156&#x27E9;<\/a><\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-01098929\/file\/AotStr__2014.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-01098929\/file\/AotStr__2014.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-01098929\/file\/AotStr__2014.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-01098929v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='SousRubrique'>Preprints, Working Papers, &#8230;<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-00956769v1\" target=\"_blank\" >Building explicit induction schemas for cyclic induction reasoning<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\">2014<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-00956769\/file\/document.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-00956769\/file\/document.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-00956769\/file\/document.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-00956769v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2012<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-00764909v1\" target=\"_blank\" >Performing Implicit Induction Reasoning with Certifying Proof Environments<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Amira Henaien, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>SCSS&rsquo;2012 &#8211; 4th International Symposium on Symbolic Computation in Software Science<\/i>, Dec 2012, Gammarth, Tunisia<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-00764909\/file\/document.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-00764909\/file\/document.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-00764909\/file\/document.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-00764909v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-00763236v1\" target=\"_blank\" >A Unified View of Induction Reasoning for First-Order Logic<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Turing-100, The Alan Turing Centenary Conference<\/i>, Jun 2012, Manchester, United Kingdom<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-00763236\/file\/document-poster.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-00763236\/file\/document-poster.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-00763236\/file\/document-poster.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-00763236v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2011<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/hal-00644876v1\" target=\"_blank\" >Automated Certification of Implicit Induction Proofs<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat, Vincent Demange<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Certified Programs and Proofs<\/i>, Dec 2011, Kenting, Taiwan<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/inria.hal.science\/hal-00644876\/file\/document.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/inria.hal.science\/hal-00644876\/file\/document.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/inria.hal.science\/hal-00644876\/file\/document.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/inria.hal.science\/hal-00644876v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<p class='Rubrique'>2010<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/inria.hal.science\/inria-00525187v1\" target=\"_blank\" >Integrating Implicit Induction Proofs into Certified Proof Environments<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Integrated Formal Methods &#8211; IFM 2010<\/i>, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.320-335<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au bibtex<\/dt>\n<dd class=\"ValeurRes LienBibtex\"> <a href=\"https:\/\/inria.hal.science\/inria-00525187v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-00553078v1\" target=\"_blank\" >Good reasons to implement transnational European diploma programs in Computer Science<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Gabriel Michel, Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>ICEUTE&rsquo;2010 (First International Conference on EUropean Transnational Education)<\/i>, 2010, Spain. pp.135-143<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-00553078\/file\/MicStr_2010.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-00553078\/file\/MicStr_2010.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-00553078\/file\/MicStr_2010.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-00553078v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl>\n<dl class='NoticeRes'>\n<dt class=\"ChampRes\">titre<\/dt>\n<dd class=\"ValeurRes Titre\"><a href=\"https:\/\/hal.science\/hal-00553070v1\" target=\"_blank\" >Integrating Implicit Induction Proofs into Certified Proof Environments<\/a><\/dd>\n<dt class=\"ChampRes\">auteur<\/dt>\n<dd class=\"ValeurRes Auteurs\">Sorin Stratulat<\/dd>\n<dt class=\"ChampRes\">article<\/dt>\n<dd class=\"ValeurRes article\"><i>Integrated Formal Methods<\/i>, 2010, France. pp.320-335<\/dd>\n<dt class=\"ChampRes\">Acc\u00e8s au texte int\u00e9gral et bibtex<\/dt>\n<dd class=\"ValeurRes Fichier_joint\"> <a href=\"https:\/\/hal.science\/hal-00553070\/file\/Str_6396_2010.pdf\"  target=\"_blank\"> <img decoding=\"async\" alt=\"https:\/\/hal.science\/hal-00553070\/file\/Str_6396_2010.pdf\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_pdf.png\" border=\"0\" title=\"https:\/\/hal.science\/hal-00553070\/file\/Str_6396_2010.pdf\" \/><\/a> <span class=\"LienBibtexACoteFulltext\"><a href=\"https:\/\/hal.science\/hal-00553070v1\/bibtex\" target=\"_self\"> <img decoding=\"async\" alt=\"BibTex\" src=\"https:\/\/haltools.inria.fr\/images\/Haltools_bibtex3.png\" border=\"0\"  title=\"BibTex\" \/><\/a> <\/span><\/dd>\n<\/dl><\/div>\n<p> <\/body> <\/html> <\/p>\n","protected":false},"excerpt":{"rendered":"<ul>\n<li>\n<a href=\"http:\/\/dblp.uni-trier.de\/pers\/hd\/s\/Stratulat:Sorin\">DBLP<\/a>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<p>Publications depuis 2010<\/p>\n<p>&nbsp;<\/p>\n<p>               var _paq = _paq || [];   _paq.push([&lsquo;trackPageView&rsquo;]);   _paq.push([&lsquo;enableLinkTracking&rsquo;]);   (function() {     var u=\u00a0\u00bb\/\/piwik.inria.fr\/\u00a0\u00bb;     _paq.push([&lsquo;setTrackerUrl&rsquo;, u+&rsquo;piwik.php&rsquo;]);     _paq.push([&lsquo;setSiteId&rsquo;, 25]);     var d=document, g=d.createElement(&lsquo;script&rsquo;), s=d.getElementsByTagName(&lsquo;script&rsquo;)[0];     g.type=&rsquo;text\/javascript&rsquo;; g.async=true; g.defer=true; g.src=u+&rsquo;piwik.js&rsquo;; s.parentNode.insertBefore(g,s);   })();  <\/p>\n<p><img decoding=\"async\" src=\"\/\/piwik.inria.fr\/piwik.php?idsite=25\" style=\"border:0;\" alt=\"\" \/><\/p>\n<p>   Publications HAL de  Sorin, Stratulat   <\/p>\n<p class='Rubrique'>2025<\/p>\n<p class='SousRubrique'>Conference papers<\/p>\n<p>titre<br \/>\n<a href=\"https:\/\/inria.hal.science\/hal-05447018v1\" target=\"_blank\">AIROBO: A EUROPEAN PROJECT FOR SOFTWARE ENGINEERS<\/a><br \/>\nauteur<br \/>\nI Dramnesc, E Abraham, N Fachantidis, T Jebelean, G Kusper, Sorin Stratulat<br \/>\narticle<br \/>\n<i>EDULEARN 2025 &#8211; 17th International Conference on Education and New Learning Technologies<\/i>, Jun 2025, <\/p>\n","protected":false},"author":5,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"page-fullwidth.php","meta":{"footnotes":""},"class_list":["post-13","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/pages\/13","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/users\/5"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/comments?post=13"}],"version-history":[{"count":31,"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/pages\/13\/revisions"}],"predecessor-version":[{"id":408,"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/pages\/13\/revisions\/408"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/SStratulat\/wp-json\/wp\/v2\/media?parent=13"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}