Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Offre de thèse sémantique/preuve de programmes à l'ISAE-Supaero et l'ENAC

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Offre de thèse sémantique/preuve de programmes à l'ISAE-Supaero et l'ENAC


Chronological Thread 
  • From: Celia Picard <celia.picard AT recherche.enac.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Offre de thèse sémantique/preuve de programmes à l'ISAE-Supaero et l'ENAC
  • Date: Mon, 13 Jan 2025 17:37:19 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=celia.picard AT recherche.enac.fr; spf=Pass smtp.mailfrom=celia.picard AT recherche.enac.fr; spf=None smtp.helo=postmaster AT mailhost.recherche.enac.fr
  • Ironport-data: A9a23:0dbcnaDBlMPR4hVW/6rnw5YqxClBgxIJ4kV8jS/XYbTApD0khDEGx mIaW2qFb/aMNjT0ctlyPoiz9E0D7cODmoQ1OVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuGYjdJ5xYuajhJs/va80s21BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc52yYS0PFm9pqNlgJZbcZ5u1ILlMU0 ONNfVjhbjjb7w636LeyS+1sgd8/atPmN4MSoHpgwHfUC/8tB57ZK0nIzYYJgXFg3YYXRqiYP ZdDAdZsREyojxlnMVoTCZt4hOajj2PzWydVo1KYv6E37i7eygV6lrb3WDbQUoXSG58PwBzC/ Aoq+UzSGxAhd5+V8Aa6/1+onP3Fj2DGCbwNQejQGvlC2QHClzNDV3X6T2CTqv6gz0W6Rth3M F0R4iNorK4o9UXtQMOVYvGjiHCb+AQRUNpdCeY65UeAzKPfpQiDboQZctJfQP14jPcfHRMu7 Ea2x+noGTdQn4/PbG3Io994sgiOESQSKGYDYwoNQg0E/8TvrekPYvXnFYoLLUKlsuAZDw0c1 BiklkADa1g7g9FNzaiw/V3diDKh4JXPRwVz6B+/soOZAuFRP9fNi2+AsAazARN8wGGxFwfpg ZT8s5LChN3i9LnU/MB3fM0DHauy+9GOOyDGjFhkEvEJrmv2pSH7I94BsG8ifS+F1/ronxe0P yc/XisPvfdu0IeCMPAtC25MI51ykPa/S4SNug78MYYSM8YZmPC7ENFGPBLBjj+9zyDAYIklN JGSbcu2ZUv2+ow5pAdas9w1iOdxrghnnDO7eHwO5032uVZoTCfEEe9dWLZPB8hlhJ65TPL9q ogDZpbRlUgOCIUToED/qOYuELzDFlBjbbieliCdXrfrztNOQTl4U63i0vk6dpZ7nq9YsO7N8 zvvEgVb0VfzzzmPYwmDdnkpOvulUIddvEALG3UmHW+p/Hw/PqepzqMULKUscZcdqedM8P9TT ts+QfumPMhhcDr9xmkiXcHPl7A6LBWPriCSDhWhewk6LsJBRRSW29rKfTnP1SgpDwimh/QYp I+Q9AHSbqcedTs/DPfHNfekznKqnH0ngOkpdVD5EtpSX0TN8YZRNC36iMEsEfwMMRnuwji71 R6cJAUx/c3hgtYS3oHSpKamq4yJLbNPLnBCFTOG0YfsZDjowGWz5KRhDsCKRGn5f0Hp8vyAY e518anNAMcflgwXj7smQqdZ9oNg1d7BvLQA8x9FGk/MZFGVCr9NBHmK8M1Ml69VzI9ipgqEd ROTy+ZeJIm2FpvpIHwJKCohS9az5/Uetz3RzPYyeWHRxit8+piZWkRzYTiIrgFgL4VODYB0+ td55fYq6DG+hCE6bfeArCRfrFqXIlI6Dq4Ii5A9Aa3QsDQN9G1sW5LnJxHT3ICucPRJa0kjH S+VjvHNhpNa3UvzTEAwHnnsg8tY3JQHhwBNxgQkf3CPuN703P8z1xh39gYMEwBfyztF9+dBK 0lqKExHCqGc9Bh4hMV4fj6NGiMQIDa760DO218yu2mBdHaRV0vJN38YFd+W2UIkr1JnYTlQ+ Y+HxFbfUTrFeN/72g0wUxVHr8PPYMNQ9AqYvuyaBOWAQocHZAT6jp+UZWYnrwXtBeUzjhblo cho5ONBVr3pBxUPoqEUC5io6ppIcUqqfFd9ePBG+L8FOUr+ezvogDiHFB2XS/N3fvfP9Re1N txqKsdxTC+B7SeprA0AJKsyMrRxze8I5t0DR+vRHlQ4kYCj9xhnjJGB0RLFpj4PY85vmsMDO I/uZ2q8MmiPt0B1xU7Jjud5Y1SdX/dVRTfS/u6P9McxK6kiq8BpKEE77au1tS6aMSxh5BOlg znAbK73kc1k64BdxYvoGaBlADePdNf5UcqK1AWBovVPctL9HsPcvCwFqlTcHlp3PJlAf/9Vh LiyoNrM80edh4kPUkfdgIukO5BSwMePANpsLcP8KUdFkRu4WMPD5wUJ/0a6I8drlOxxy9aGR QziTueNbv8QBslgwUNKZxhkExoyD7r9aoHir3ifq9WOEh0s7hzVHui49HPGbXBpSQFQAsfQU jTLgveJ4sxUiK9uBxVeXvFvPMJeEW/ZAKAjc4X8iCmcAmyWmWi9g7rFlyc7yDT1G3KBQdfb4 5XEe0DETy6Mmpr0lfNXj48jmScsLidNsbFlNAZVsdt7kCuzA2M6PPwQe8dOQI1dlivpkor0f nfRZW8lEj/wRilAbQ662tn4QwODHaYbD78V/NDyE5+8ME9axb9sAYeNMg9l6nZyejz40Ke9J Noe92f7PhX3z5dgTqAd/JRXRAuhKuzynho1FYLVyqQewCryxZ0Q2XdhERBGVSGBHsfEnwPFP wDZgEhaFVqjRxeZ/dlIIhZo9dJwgN8r5y8lZieC2t3ftsOWyuRLjvPlUw02Pnvvc+xSTIMzq bjLq6dhLoxYNrH/eUfkhj7xvZJJNA==
  • Ironport-hdrordr: A9a23:F6W1bqOfWFIZ0sBcTtajsMiBIKoaSvp037BZ7TEWdfU1SKKlfq +V/MjzuSWE7Qr5O0tQ+uxoWpPgfZq0z/cciuN8UotKNzOW3FdAQrsSircKjweQeREWKdQx6Z td
  • Ironport-phdr: A9a23:QhctUBQZBZmHUJty9ip8bs7c2NpsoimVAWYlg6HPa5pwe6iut67vI FbYra00ygOSBMOCtq4P27qempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizewb65+I A+roQjRucQajohvJ6UswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalWpg+qqR5izI7OeIyaKPlwcK3SctwURWRPQ9hfWjdbDY+gd YYCFfYNMfhaooT7ulAArQG+BQ6pBO731DJHmHv23awg3O88Cw/G3RAvEMgUsHvJsd74M7sdX v6xzKnJ1zrPdetW2Tbh54fSaBAuvOqBXahufsXNyUkgCRnFgUmQqYP7JT+ayOINvHKH4OZ6W +KvkXcqpgdsqTeg2skikJPGhp4Jyl/a7yV5xp44KMC3RUN6b9CpEYZduj+VOodqQM4uXX9kt SUmx7AEupO1ciYHxZUmyhPQa/KKfIuF7xb9WOuSLjl1mX1oda+wiRu07EOuxOr8Vsyu31ZLq CpIitjMtmsX2BPN88SHUeZ9/l+71jmRzQDT7ftIIU4ulabDNZEhxKQ/mYYJvUTNBC/7nlj9g qyOdkg85+Sl7+Tqbq/lq5KSLYN4lw/zP6U0lsChAek0LBACU3aG9em+zrHv4FH1TbFQgvErn KTUv4rWKMcfq6O/HgRYzIIj6wukDze6ztsYh2QJLFNEeR2Zl4XlJ1fDK+3iA/ilmVSjijJry ujGPrL/BpXNKWDOkLL7crZ8705cyA0zzctD555OELEOPu78Wk/vu9zCEhA5MxK7z/z5B9V7z IwRRXiDAqGDMK/KsF+I4PwgI/WUaYMIvDvwK+Ip6v3ggHMjhFMQc6ik0YEJZH24APhqO0CZb mDtgtcFH2cKpA0+TOnyhVKeTzFTY3eyULgm6jEjCYKpEZ3MRpqwj7Gaxie0AIFZZmBYBVCWD Xjod5uLV+0SZyKUOMBujiYIVba7S4M50xGhrxf1y6B7IerM5i0YqZXj2cBo6+HLjxE96SR0D 9iB02GKV2x7gmQIRyYv0K9jpUx910yM3LNjg/1YENxT/+lGXh07NZ7a1ex6Csr9VhjPfteTG x6aRYCtBih0RdYsyfcPZVx8EpOslEPtxS2vVpQYk72CTKQ1+avG0zClLMt5yn+AzKgqhkMqa tFCPm2rnKV/+k7eAYfC1UuDwfX5PZ8A1TLAoT/QhVGFu1tVBVYYucTtWHkeYhCTttHl/gbZS KfoD707MwxHwMrEK61Qa9Svg08VDOz7NoH4ZGS803y1GQ7O3qmFOYHnf2QUmj3cA0EenygJ8 H2GOBI1BirnrmTXB3pgDwGneFvipNF3s2jzVUoo10ePZkxl2aCy/0seiPidQrUL37kNoisJs Th/HFun1NLbTdeGrgEncr8PKcgl7gJh0mTU/xd4IoTmL61mgQsGdB9rukr1yxhtIoBJkMwqq 2g2ihB/IqKVylhBenWV25n7fLPNQoXr1DaobaOemlTX0dLNv7wK9Ox9sFL7+gegCksl9Xxjl dhTyXqVoJvQXkIUVtrqX0A7+gIfxfmSazQh547SyXxnMLWl+j7E1dUzAeI5yxGmN95BOaKAH QX2HoUUHc+rYOAtnlGoaFoDMoUwvOY/Msenfr2e2aWiJupIhj+tjWld64BwlE+K/iE6RPSJl 5cJzveE3xeWAi/mhQTE0Ii/koRFaDcOW2unnHG1WcgBPesrJthNUzr0cKjVjp1kipXgWmBV7 gumDlICg4qyfAaKKkf6xUtW3FgWpnqunW25ySZ1mncntPn6vmSGzuL8eR4AImMOSnNliAKmK oWwjtlcREmjZhIlvAGo7kb33aNbqeJyKWDYB0lSNXuTTSkqQu6ru7yObtQaopgltSReFvy9a lmARpbnrhAa3jnoH2YYyTYyfHekoN+q+n4ywHLYJ3F1on3DfMh2zhqK/93QS8la2T8eTTV5g z3abrSlF+Gg5s7c15LKs+TlEnmkSoUWai7zi4WJqCq842RuRxy5hfG63NP9Q0A21iry1t8iU iutzl60aYTv1q38KeNsd1NkLEXx4Mp3AIp+n809gpgbn3YAzpmY5nsIl27vPM4TgPOjKipWA 2dQnZiPvVKt0VYGTDrB34/jU3SB3sZtL8K3ZG8bwGN17sxHDruV8K0RmCJ0plSiqgeCBJo11 jwZyPYo9Dsbm7RQ6Vdrnn7bW+tMWxMFZ3+J9VzA9d21oaRJaXz6dLGx0BE7htW9FPSZpRkaX n/le5AkFCs278NlMVuK3megj+OsMNTWc98XsQWZ1hnaiO0AYpk8kvsDwzJmMmvnsVU/xuU7g AZl3Zz8sY6OICNj5ujqZ3wQfi2wfM4V9jz32OxVk8KX1sa3H55oADkjRpbjTf+yGzIf8/nhP g3IHid2+RL5UfLPWASY7klhtXfGFZumYmqWKHcuxtJnXBCBJUZbjVNcTHAgk5U+DAzv2N35f RIz+GUK/lCh4EgpqKogJ1zlX2zYvgvtdjokVM3VMk9N9g8br0LFec2GsrAqTnwersbn9VfTb DbGPWEqRSkIQhLWXQi7Z+vwu4GSrbbAD7jkd6OcM7uA4e1GC6XRlM/pgtAgpm3ScJ7qXDEqD uVliBAbBSkrRZqByWtREyVFy3iVN5zJ/13UFjRfiMe5/byrXQvu4dDKEL5OKZB0/Ajwh66fN umWjSI/KDBC15pKy2WagL4YlEUfjS1jbVzPWfwJqDLNQaTMm6RWEw9TaiV9M9FN5r492Q8FM NDSi9f83Lp1xvAvDFINWVvkk8CvLcsERgP1fEvAH1qOPa+aKCfjxsj2ZaO7UqEWluhftxCqs jaWVULlNz/FmSOoHxGjPOdQjT2KaRxTvIbuF3QlQWPnTd/gdli6KIou3GBwkeZy3yiUczRBa 2sZEQsFtLCb4CJGj+8qHmVA6iEgNuyYg2OC6PGeLJ8KsPxtCyAyluRA4X18xaEGiUMMDPFzh ibWqcZj5l+8lezagDFqVBtH7C5Kj4uRsW14NK7Z+4NLWXuC8RQE5iOeEV5ZwrktQs2qoK1Wx tXVwejrLyxe9tvP4cYGL83dKcaHN2E9dwDkEz7ZFgAFQHimM2jUwUJH2qL3lDXdvt0xrZ7in 4ALQ7lQWQkuF/8UPU9iGcQLPJZ9Wj5MeVuzlsMD5XekpxncAshct5uBWOjAWZ0HyR6chLhAZ xwT3fXiII8TO5fw20EkZ19zl8LEARiINTiiijdsZQ85uk5N/T5zSGQ4nUz/OFrF3Q==
  • Ironport-sdr: 67854141_IqB7BCTAWpO/LM3OcJ6Wb47/f2O8C2tsNdIJxeiUbs7HgnA /uLDeGYcv7RbdMxborDLfrl7F3ql9SfiACrVQGA==

------- Désolée pour les réceptions multiples -------

Bonjour à tous,

Les équipes CASC (ISAE-Supaero - https://www.isae-supaero.fr/fr/recherche/departements/ingenierie-systemes-complexes/groupe-ingenierie-pour-les-systemes-critiques-460) et LII (ENAC - https://lii.enac.fr/), cherchent à recruter conjointement un.e doctorant.e pour une thèse financée pendant 36 mois, débutant à l'automne 2025 (financement acquis). Cette thèse pourra être précédée d'un stage de M2.

La thèse portera sur la formalisation et la vérification de la sémantique d'un langage dédié à la création de systèmes interactifs (UIDL) avec l'assistant de preuve Coq. Le sujet exact est "Formalisation et la vérification d’un UIDL formel bigraphique dans Coq". Ce sujet s'intéresse particulièrement aux systèmes interactifs critiques (ie, ceux qui sont en interaction avec un être humain), mais la thèse se situe plutôt dans les domaines de la sémantique des langages et de la preuve de programmes. Le ou la candidat.e devra démontrer une forte appétence pour ces sujets.

Tous les détails (en particulier les modalités de candidature) sont ici : https://cloud.recherche.enac.fr/index.php/s/GzdBcG9WZskHiY4/download

N'hésitez pas à me contacter pour toute information complémentaire et à diffuser largement cette offre autour de vous,

--
Signature mail

Celia PICARD
Associate Professor
Interactive Informatics Team

Ecole Nationale de l'Aviation Civile
7, Avenue Edouard Belin - 31055 Toulouse cedex 04

Tel : (33) (0)5 62 17 42 21
www.enac.fr








  • [Coq-Club] Offre de thèse sémantique/preuve de programmes à l'ISAE-Supaero et l'ENAC, Celia Picard, 01/13/2025

Archive powered by MHonArc 2.6.19+.

Top of Page