Robbert Krebbers
2018-11-07 19:30:06 UTC
The Programming Languages group at Delft University of Technology is
looking for:
- One PhD student (4 years)
- One post-doc (1 year)
The topic of research, which will be determined based on the common
interests of the candidate and the supervisor, will be in the
development of expressive program logics for:
- Verification of multilingual software
- Verification of asynchronous I/O
- Verification of non-functional properties (time/space/security
properties/...)
- Verified compilation
This work will revolve around Iris <https://iris-project.org/>: a
higher-order concurrency separation logic framework that is implemented
in the Coq proof assistant <https://coq.inria.fr/>. Iris has been
successfully used for a variety of applications including but not
limited to logical-relations for relational reasoning, program logics
for relaxed memory models, program logics for object capabilities, and a
safety proof for a realistic subset of the Rust programming language.
The successful candidates will work under the supervision of Robbert
Krebbers <https://robbertkrebbers.nl> and Eelco Visser
<https://eelcovisser.org/>.
# Requirements for the PhD position
- A master's degree (or equivalent) in computer science, with a strong
interest in program verification, proof assistants, and program semantics.
- A strong commitment to research.
- Previous experience with Coq or separation logic is preferred, but not
necessary.
# Requirements for the post-doc position
- A PhD degree in computer science, in a topic related to program
verification, proof assistants, and program semantics.
- A strong publication record.
- Previous experience with Coq and separation logic.
- Previous experience with Iris is preferred, but not necessary.
# Application instructions
More information about the vacancies and information how to apply can be
found at:
- PhD student:
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50824/?lang=en
- Postdoc:
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50825/?lang=en
The starting date of both positions will be decided with the candidate
(earlier dates are preferred).
Informal inquiries to Robbert Krebbers <***@robbertkrebbers.nl> are
welcome.
looking for:
- One PhD student (4 years)
- One post-doc (1 year)
The topic of research, which will be determined based on the common
interests of the candidate and the supervisor, will be in the
development of expressive program logics for:
- Verification of multilingual software
- Verification of asynchronous I/O
- Verification of non-functional properties (time/space/security
properties/...)
- Verified compilation
This work will revolve around Iris <https://iris-project.org/>: a
higher-order concurrency separation logic framework that is implemented
in the Coq proof assistant <https://coq.inria.fr/>. Iris has been
successfully used for a variety of applications including but not
limited to logical-relations for relational reasoning, program logics
for relaxed memory models, program logics for object capabilities, and a
safety proof for a realistic subset of the Rust programming language.
The successful candidates will work under the supervision of Robbert
Krebbers <https://robbertkrebbers.nl> and Eelco Visser
<https://eelcovisser.org/>.
# Requirements for the PhD position
- A master's degree (or equivalent) in computer science, with a strong
interest in program verification, proof assistants, and program semantics.
- A strong commitment to research.
- Previous experience with Coq or separation logic is preferred, but not
necessary.
# Requirements for the post-doc position
- A PhD degree in computer science, in a topic related to program
verification, proof assistants, and program semantics.
- A strong publication record.
- Previous experience with Coq and separation logic.
- Previous experience with Iris is preferred, but not necessary.
# Application instructions
More information about the vacancies and information how to apply can be
found at:
- PhD student:
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50824/?lang=en
- Postdoc:
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50825/?lang=en
The starting date of both positions will be decided with the candidate
(earlier dates are preferred).
Informal inquiries to Robbert Krebbers <***@robbertkrebbers.nl> are
welcome.