coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Two PhD Positions in Program Verification

From: Amin Timany <amintimany AT gmail.com>
To: types-announce AT lists.seas.upenn.edu, coq-club AT inria.fr, agda AT lists.chalmers.se, categories AT mta.ca, logic AT math.uni-bonn.de, lean-user AT googlegroups.com, homotopytypetheory AT googlegroups.com, eutypes AT cs.ru.nl
Subject: [Coq-Club] Two PhD Positions in Program Verification
Date: Wed, 25 Jul 2018 10:31:34 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=amintimany AT gmail.com; spf=Pass smtp.mailfrom=amintimany AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f51.google.com
Ironport-phdr: 9a23:pPPsDRSEDUaYGiCDP1T1HJfh79psv+yvbD5Q0YIujvd0So/mwa67ZBKAt8tkgFKBZ4jH8fUM07OQ7/i+HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9zIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlsN/g79VrhGvqRJhxIDZe5uaOOZ7fq7HfdMWWWhMU8BMXCJBGIO8aI4PAvIdMOZdron9oUYFowW/BQmpHuzvzD9JjWLx0KIg1uQhEAfG3BAhH9ILqnvUqtX0ObwdUeCw1qbIzDHDY+lK1jf67YjFaxYsquyCU7J3dMre00gvFwXdg1WTtIzlOy2a1vkTs2eF6epsT/mghHA/pwFwpDiv3MYshZPTioIb0FDI7SR5wJw0Jd2jUUJ7ecSkEJxSty6EK4R2XtkuQ2ZyuCY10rEGtp+7fDQKyJQ63BHTceCIc4+N4h/lSe2fIi94iWp7dL6jgxu+60utx+3mWsWqzFpHrTBJn9nRunwVyRDc8NSLRuV480u82juDyh3f5+RYLkwpm6rWLpEszqMsmpYPtEnOHTL6lUXygaKTakoo5+ml5uXib7n4vZCRM5J4hwTjPagzh8CyD+I1ORUUUWeB4+Szzrjj8FX5QLpUiv02lbHUsJXAKsQaoq61GhFa3Zs+5xqmATer0MkUkWMILFJCfxKHgIzpNE/ULP/kCve/hkygkDZtx//YIr3sGovBImTHnbv7frtw61RQxBQvwd1c/Z5ZCqwNLOr2WkDrtdzYChE5Mxazw+biENhyzIYeWWOJAq+FMaPStEWH5uQvIuSXa48VvSzyK/kh5/L0kXA5nlodcbGz3ZQLcHC4AuhmI0KBbHXwhdcBCH4GsRY6TOz3k1KPSiVTZna3X6Ik/D43EoOmDYHZRoCsmrONxim7HocFLlxBX0ydCXrzMoyCXfARbimfCstgiSAfE6OsQpRnyAmjsgm8xrZ6aqLf/TRdvpb+3vB04ffSnFc873g8BsuR2kmJTnpohSUDRzYy2a1lugpmxxPL2qFkjvNfD91e/NtMTg58PpeYh+h9BNH5cgfIYtfPVVCnB9+hBzd3Qt91i9sDakA4Bs6vlDjM2C2lB7IajbuWHIdy+aXZmzDxIMN613HexbUwl1Q6QsZIL3yOial4+AzeCJTOjl2C0a2tcOBU0TPR5X+O1kKFpwdCTUh2VfbrR3caM2LTrNKx2kLHRrm/QeAuNwpH1c+HI61bQtLshFRCAvzkPYKNMCqKh26sCEPQlfu3Z43wdjBFhXSPOA0/iwkWuE2+G007DyalrXjZCWU3R13qakLot+J5rSHiFxNm/0Sxd0RkkoGN1FsNn/XFEqEc27sFvGEqrDAmRA/gjeKTMMKJok9aRIsZYd455w0ah2fQtgg4M5D5aq4/3xgRdAN4u06o3BJyWN1N

Please feel free to further disseminate this announcement and forward it to whomever would be interested.

Online version: https://distrinet.cs.kuleuven.be/jobs/#program_verification

PhD Positions in Program Verification

We have two open PhD student positions in the program verification group. These positions involve performing research on program verification under the supervision of Prof. dr. Bart Jacobs and postdoctoral researcher Amin Timany, with the goal of obtaining a PhD within four to five years. PhD students are expected to publish and present their results regularly at competitive international conferences and journals, which generally involves international travel, as well as to contribute to the Department's educational obligations. Possible topics include:

• Logical techniques known as "logical relations" for proving properties of advanced programming languages and programs written in those languages, such as compiler correctness, compiler security, correctness of optimizations.

• Developing advanced program logics for reasoning about correctness of higher-order programs with fine-grained concurrency.

• Developing supporting theories, such as type theory and category theory, to serve as logical and semantic foundations for program logics

• Developing supporting tools, such as proof assistants (e.g. Coq, Agda) and program verification tools (e.g. Iris, VeriFast), including advancing their usability by developing improved automation technologies.

Links:

• Coq: https://coq.inria.fr

• Iris: https://iris-project.org

• VeriFast: https://github.com/verifast/verifast

• Prof. dr. Jacobs: https://distrinet.cs.kuleuven.be/people/bartj

• Dr. Timany: https://distrinet.cs.kuleuven.be/people/amin

Profile:

• Strong background in computer science (Master's degree or equivalent)

• Strong background in mathematical logic and/or theoretical foundations of computer science

Interested? Contact Prof. Bart Jacobs (bart.jacobs AT cs.kuleuven.be) & Dr. Amin Timany (amin.timany AT cs.kuleuven.be) no later than September 30, 2018. Do not hesitate to contact us if you have any questions regarding these open positions.

[Coq-Club] Two PhD Positions in Program Verification, Amin Timany, 07/25/2018