coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] PhD Position: Verification of Golang using Interactive Theorem Proving (Application Deadline 2025-02-10)
Chronological Thread
- From: "Achim D. Brucker" <adbrucker AT 0x5f.org>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] PhD Position: Verification of Golang using Interactive Theorem Proving (Application Deadline 2025-02-10)
- Date: Tue, 4 Feb 2025 11:02:14 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adbrucker AT 0x5f.org; spf=Pass smtp.mailfrom=adbrucker AT 0x5f.org; spf=None smtp.helo=postmaster AT smtp.0x5f.org
- Ironport-data: A9a23:XnYb6K87rza3O94oQmD7DrUD93qTJUtcMsCJ2f8bNWPcYEJGY0x3x 2dJWjqGP/aOZWaje4wjbo7n8k8FsMfSz4cyHQNrrStEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWcvWo4ow/jb8k435qyu4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE2ulMNlhxYpYi38ltXExw7 NcgF2ADYUXW7w626OrTpuhEncE/NI+zLN4R/HZ6wlk1D956HNaaGP+Mv4MFmm1o2aiiHt6GD yYdQTNjZg7daB5CIH9PGM8w2uCyiRETdhUC8AzJ9PJosjW7IApZgIS9aIuNKvGzYuZ0gliJv nuXw0v2K0RPXDCY4WDdqS/07gPVpgvwX5tXH7ml/NZxkViLzyoSDgcXXB21u5GEZlWWQNdDM wpM6ncg668o+yRHU+URQTWhvFy+p1lDQOB1PPdnxT+U4ZLrswiWUz1soiF6VPQqs8o/RDoP3 1CPns/0CTEHjFFyYSvGnop4vQ+P1T4pwXgqSQJscOfoy8LmvJl11gKSQJBkCqHdYjzJ9dPYm W/iQMsW3e97YSs3O0KTpAuvvt5UjsKVJjPZHy2ONo9lhysgDGJfW6Sm6ELA8dFLJ5uDQ1+Ks RAswpfFvL5WUszVyXHQHI3h+Y1FAd7aaFUwZnYwR/EcG8iFoCL9I+i8HRkuex81aq7ohxe0P R+N0e+u2HOjFCHyNvIvC25AI8In0aP9DZzqU/rUBueikbAuHDJqPUhGOyat4owauBN3yvxhY 8/DIZ/E4LRzIf0P8Qdajtw1idcDrh3SD0uKLXwi50X6geitdzSORK0bMVCDSOk84enW6E/W6 ttTfY/CgRlWTOS0MGGd/J8xPGI6CyExJan3jMhLKc+FAA5tQ186B9HrnLgORo1CnoZurNnuw E2TYEFi9QfAtSX1EjnSMnFHQ5HzbKl7tkM+bHANP073+n0NYrSPzaY4droocJUZ8chmnO9GX tgeWsC6Gv8UYC/2yzccSpjcrYJZaxWggzyVDReleDQSe51BRRTD393ZIjvU6ygFCxSoufsEo 7GP0h3RRbwBTV9ACPn6Re2OzVTrm1Qgg8N3AlX1J+dMdHXW8IRFLzL7itk1KZouLTTB3j6r6 BaEMywHpOXio54Hz/eRvPqq97yWKupZGlZWO0L57rzsbCnTwTeF8L96Ce2NeWjQaXPw9KCcf t5q9vDbMsAcvVN0ooF5QqdKz6U/2oPVnIVk7D9YRVfFU1f6LYlbACii/dJOvahz1LNmqVOIe kaQyOJ7Z5SNGu3YSWA0GiR0T96+xck1mybT58sbOE/VxjF615vZXFRwPyujsj18Lrx0O9l8m ewK5NEbxzK6rh97I+SXrzt18l6UJScqSJQXtZA9Aa7qhDE0y1pEX4fuNy/u7LyLaPROKkMPM BbNoIbj3pNynlHjdVg3Hljzhdttv4wE4k12/QVTNma3lcrgrd5p+h9oqBAcbBlflzdD2MJNY llbDVV/f/iyzm05lfp4fj6eHi9aD0ek4W338VwCkVPZQ2SOVmDgKG4cO/6HzHsG8lBzLyRqw 7WF9FnLCTraXtn9/i8Xa35Xr/bOSd9Q9AqbvOuFG8+DPYcxYBu7o6uISFcLlSDaApIKtBWan dVpwed+Ur2kFCgyp6ZgNZKW+45NQz+5JUtDY8pbwoU3IU/mdgqf4wO+c3KKRpsVJtjh01OJN Mh1F8ceCzW8zHmvqx4YN44tIph1veEkyOQHXra6NFwXkqC+qwBxu8n67RnOh24MQvRvn/0iK 4jXSSmwL2yIiVZQmE7PtMNhOFfkUeIbZQb54v+5wN8JG70HrutoV0M4iZmwgFm4Lypl+Eiyk D7YRqqL0dFn95tgr7HsHopHGQ+wD9H5D8aM0QKrtuVxfcH9CtjPuywVu2vYEVxvZ5VJYOtOl JOJrNLT92HGtuxvU2nmxr+wJ5MQ7sC2BOdqIsb7KUdBphS7Weju3gAi/l6pIpkYgfJf4ciaH zGDUvWSTuJMedlhxyxyURN8QiYtU/G9Ku+qoC6mtP2DByQMyQGNfpvt6XbtanodbSMSfYH3D gjvofu1+9REt8J2CQQZA+19SYpNSLM5tXDKq/Wq3dVZMoWpvr9GkqDniQJmsSGWBD+DCsmSD VcpgPThXEzahU0K5IgxX09OUtk/VGYgj683ZE11FxtelWWhFGBfRQgCGcxuN3yX+xAeELmgd GzDKmw4Bk0RmNiCnQrUuLzeY+tUOgDC1hoV6NDkE4N4phpa3L+9PYY=
- Ironport-hdrordr: A9a23:Ix5HW60lwvJ+8MVe/ZehhgqjBLokLtp133Aq2lEZdPVwSL39qy nOpoV/6faQsl0ssR4b9exoVJPufZq+z+8W3WByB9eftWDd0QPDQb2KhrGC/9SPIUPD398Y6Z xEGpIOa+HNMQ==
- Ironport-phdr: A9a23:6cBsPxHy6DychPVYdPB8RJ1Gf1BGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k21hmRBc6Bs6kfw6qO6ua8AjVGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdW Pp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uM Rm6twrcu8cIjYd4Nqo91hTFrmVUd+lYy25jOFafkwrh6suq85Nu/Tlct+g9+8JcVKnxYrg1Q 6FfADk6PG8549HmuwPEQQWT+HUXT38YkgBPAwjL7RH6Won+vy7nvedj2yeUINP7Q6ksVTut8 6lkRhnoiDwaNzEi62HYltZwjKNArx2/oRF03pPZb5uUNPp6eaPdYM8aSG9cVctfSyBNHoWxZ JYJAuEcP+hXspP9qkMAoxW+GweiGeDhxTBUiXDrxqA6z/gtHxra0AA8A94DsnLZp8j1OqcIV uC1ybHFwTvfYvxK2Tf96Y3IeQ0vr/2WQLl9bNDRyVQzGAPGkFqQs4LpNC6S2+sXrmeU9PBgV f+zhG4ktQ5xuCOiytsji4TJiIIZ0FfE9T92wIssI9CzVUF0b8K+HpRKqyGaK5V5QtkkQ2xwu ys0xKAKtJCmcCUJ1JkqwxrSZvyJfoWG7BzuW+icLDV5iXxle7+zmhS//0i+x+DyVsS63ktGo jZFn9XQtn4AyRre4dWJRPt6+0euwzeP1wbL5+5aLkE7i7bbJIA7wrIqjJUcrV7PHjL1mEnul 6CWbFgk9fSr6+v5eLXqvIOTN49shgH6NaQulc2/DvgiPQgKX2iU4/iz1L7i/U3/T7VGlOE5k q7csJ3cOM8Vpba5Dhda34sj8RqzEjmr3MoCkXUZI19IeAiLg5b1N1zMOPz0EPiyjlu2nDt2x f3LMKftDovNI3XDirvtYLdw5kFaxQEu091f449UCqodIP3tQE//qd3YDx4nPAGs3urqDsh22 JkEVmKVGKCZNbvfsV+W6eIrJOmBfJQVuDPhK/g9/fLikXA4lF8TfaWz2psXcn+4EuxnI0Wff 3Xsns8MHGgKswYkUeDnhkOOXSRNa3u9X68w/C83BJ6kAIvbQ4Cimr2B3CO1Hp1MYWBGD0iBH m31eIqfQfcMdT6dIsx/nTweTrWtV4Ag2BGgtAPgzLpnNOXU9jUetZ34zNd1/fHclQku9TxoC MSQy3yBQ3lunmwUXz82wLx/oUtlx1if1qh4muVUGsBX5/NUSQg3LoXczux/C9DqQA3NZNaJS FC8QtWnGz49VNwxw8VdK3p6Tt6ll1XI2zegK74Tjb2CQpIuoYzG2H2kbe92y3fDnIVnx3M8X 8BMOHfszvp2+wLJGoXKnl+xz7b3e+IbxiGbpzTL9naHoEwNCF04aq7CR31KPiM+zPz870LGF fq1DKg/dxFGwoiEI7dLbdvgiRNHQu3iMZLQeTH5gH++UDCPwL7Ed4/2YyMFxiyIAUQOiR0Y/ nucHVAuWynnpHjRX3R1DVy6W0r36qFlrW+jCEo9zgWEdUpkgrO58AQIjv+RUdtLzu8K/iA7p GY8B06zivTRDdfIvA99ZONcbNc6tU9Azn7cvhdhM4aINKV+nhhGY1l5+UT02H2bE61mls4n5 DMvxQt2c+eD1U9ZMimf1tb2M6HWLW/7+FaubbTX0xfQyoTe/KBH8/k+p1j52WPhXkM/73Vq1 cVU2HqA993LCgQVS5f4Tkcw8VBzubjbZiA3446c22drNOG4tTrL2tRhA+VAqF7odttVKr6PF wLoO5UKWsboL/Yl2hCoYh8CIOFO5fssJcr1P/CC2aOtIKNhhGf60CIeu9o7iB7RsXAkFb2tv d5N2fyT0wqZWi2piV6gtpqygoVYfXQIGWH5zyH4BYlXb6k0fIARCG7oLdfko7c2z5PrRXNc8 0auQl0c38r8MxOeZUbg1g5dz2xPsSGp3yyiwHYn9lNh5rraxyHIz+n4IVAONmRRWWJhgE3Ee ZjpgZYdRkfiPEA50RCi40j93a1Soq9yenLSTUl/dC/zN2h+U6G0u9JueuZ34Ygz+WVSWeW4O xWBT6Ll5gEd2GXlFndfwzYyc3ervI/4llp0kjDVIHF2pXvfMcZ+oHWXrNXQT+RM1TkLXgEgm WTZQF+mMJGl8M6VmJHKru2lHz78EMQIK2+xkd7G7nPkrWRxSQWyhfWyhsHqHW1YmWfg2t9mW D+J5Bfwb4/31rirZOduf01mHlj5uIJxHoBzlJd1hYlFhSVc387PuyBbzCGpaYoIvMC2JGAAT jMK3dPPtQ3s2Uk5a2mM25q8THKWhM1oe9i9ZGoSnCM79cFDTqmOv9km1WN4pES1qQXJbL1zh DAYnLEn5HQAnuoKtRAFljXADPYVB0YSbkmO31yYqsuzqqlafjPleLS6zld1nt27JOmS/w8aX 2z2MMRqDWp76cNxN0jJ2Xv459T/edXeWtkUswWdjxbKi+UGTfB53upPnydsPnjx+GE00+Nux wI7xom05cLUY3Uo5q+yBQRUcyH4d99GsC+4lr5Qx46fjZuqAo0nQiVWUt3vV/3NcnpatOy7Z VrTVmRn8DHBReeZR1fAoE4uqmKHVpmvMzv/yGAx69JkSVHdIUVehFpRRzAmhtsjEQvswsX9c UB/7zRX51jiqxIKxPg6fx/4GnzSogulcFJWANCWMQZW4wde5kzULd3W7+R9GDtd94GgqwrFI 3KSZgBBB2UEEkKeAFWrMr6r7NjGu++WY4j2Z+PJeqmLoPdCWu2g3pezys0+72uCcMKVMTgqD vE23FZCQWEsG8ndnGZqKWRfnCbMYsiH4Rakr3Eq6JnkqrKxBF+pv9PQWN4weZ119hu7gLmOL buVjSd9c3ND048UgGXPw/4Z1UITjCdnc3+sF64BvGjDVvG1+OcfAhgFZid0LMYN4bg721wHM MLRkM7+1bNipqYlVlkDUkbu0JLMB4RCMySmOVXLCVzefqyBPiHOytrrbLmUUrhMlKMMp0C+/ zGBHAWwW1bL3ymsXBepP+ZWiSidNxELo4CxfCFmDm37Rc7nYBm2WDeSpWUmnLNygWnFZzZ02 dlUaEZRtvvI/X5WxPJlFD4ZhpKKBbGUxijf6PPXeM9+jA==
- Ironport-sdr: 67a1f3b9_+DbI+bOZB8qOHcQ7t7hfy46fF9ET/xptEsRbp3Hjit22E01 JARaNHk/7AnNSYdjq+S7VRwiBjVWAScZPfgtBLQ==
We have an exciting funded opportunity for a PhD on developing "Verification
Environment for Distributed Systems Implemented in Go". The main objectives
are to define a formal semantics of Go and its CSP-inspired concurrency model
in an interactive theorem prover (e.g., Isabelle/HOL) as well as developing a
calculus for program verification. This is a unique opportunity to work in
the intersection of theory and application and while doing so, contributing
to improving the state of the art in software correctness and security.
A detailed description of the PhD proposal is available at:
*
https://www.exeter.ac.uk/v8media/recruitmentsites/documents/A_Verification_Environment_for_Distributed_Systems_Implemented_in_Go_EPSRC_DLA_Project_September_2025_Entry.pdf
Information about the funding and application process is available at:
* https://www.exeter.ac.uk/study/funding/award/?id=5477
Application deadline is the midnight GMT on 10th of February 2025.
Please reach out to me, if you have any questions.
Best,
Achim
--
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of
Exeter
https://www.brucker.ch | https://logicalhacking.com/blog
@adbrucker | @logicalhacking
- [Coq-Club] PhD Position: Verification of Golang using Interactive Theorem Proving (Application Deadline 2025-02-10), Achim D. Brucker, 02/04/2025
Archive powered by MHonArc 2.6.19+.