Logic List Mailing Archive

PhD student position in formal verification, Delft (The Netherlands), Deadline: 1 Apr 2019

The Programming Languages group at Delft University of Technology is 
looking for:

   A fully-funded PhD student (4 years) on formal verification

# Description

It is important to develop software that is robust, fast, faultless, and 
secure. Formal verification is an effective way of establishing that 
software enjoys certain properties (e.g. it does not crash, does not have 
data-races, behaves according to some protocol or mathematical 
specification) for all possible inputs. Over the last years, significant 
progress has been made in formal verification of challenging programming 
concepts such as pointers, (fine-grained) concurrency, higher-order 
functions, modules, etc. However, there are still many important concepts 
that have received conceivably less attention, such as:

- Multilingual software (e.g. foreign function interfaces),
- (Asynchronous) input/output (e.g. communication with peripheral devices),
- Non-functional properties (e.g. time/space/security properties/...).

You will work on developing next-generation formal verification techniques and 
tools for programming concepts such as the ones mentioned above. The exact 
research direction which will be determined based on the common interests of 
the candidate and the supervisor.

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. 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 candidate will work under the supervision of Robbert Krebbers 
<https://robbertkrebbers.nl/> (daily supervisor) and Eelco Visser 
<https://eelcovisser.org/> (promotor).

# Requirements

- You hold a master's degree (or equivalent) in computer science or 
mathematics, or expect to obtain such a degree soon.
- You are interested in logic, semantics, and programming languages.
- You have a strong commitment to research.
- Previous experience with Coq is helpful, but not required.

# Application

I will be considering applications until the position is filled (applications 
before April 1 are preferred). If you are interested in one of the positions, 
do not hesitate to contact me directly at r.j.krebbers@tudelft.nl for any 
information.

Formal applications can be submitted at 
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50824/?lang=en

The starting date will be decided with the candidate (earlier dates are 
preferred).

# Conditions of employment

TU Delft offers a customizable compensation package, a discount for health 
insurance and sport memberships, and a monthly work costs contribution. 
Flexible work schedules can be arranged. An International Children's Center 
offers childcare and an international primary school. Dual Career Services 
offers support to accompanying partners. Salary and benefits are in accordance 
with the Collective Labor Agreement for Dutch Universities.

As a PhD candidate you will be enrolled in the TU Delft Graduate School. TU 
Delft Graduate School provides an inspiring research environment; an excellent 
team of supervisors, academic staff and a mentor; and a Doctoral Education 
Program aimed at developing your transferable, discipline-related and research 
skills. Please visit https://www.tudelft.nl/phd for more information.

# The organization

The Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) 
of TU Delft is known worldwide for its high academic quality and the societal 
relevance of its research programs. Offering an international working 
environment, the faculty has more than 1100 employees (including about 500 PhD 
students) and more than 3000 bachelor?s and master?s students. Together they 
work on a broad range of technical innovations in the fields of electrical 
sustainable energy, microelectronics, intelligent systems, software technology, 
and applied mathematics.

The Software Technology (ST) Department is one of the leading Dutch departments 
in research and academic education in computer science, employing over 150 
people. The ST Department is responsible for a large part of the curriculum of 
the bachelor?s and master?s programs in Computer Science as well as the 
master?s program Embedded Systems. The inspiration for its research topics is 
largely derived from technical ICT problems in industry and society related to 
large-scale distributed processing, embedded systems, programming productivity, 
and web-based information analysis.

The Programming Languages Research Group is an internationally leading research 
group in programming languages, and active in areas such as language 
engineering, language design, domain-specific languages, software verification, 
and program logics. The section employs over 15 people, including academic 
staff, around 10 PhD students, and two postdoctoral researchers. The group is 
responsible for programming and programming languages education at the bachelor 
and master?s levels in the TU Delft Computer Science curriculum.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam