[DMANET] PhD position in Eindhoven on formal verification and GPU computing

The Model Driven Software Engineering section at Eindhoven University of Technology (TU/e) offers one PhD position on the development of GPU accelerated symbolic model checking techniques, within the NWO TOP project:

GEARS: GPU Enabled Accelerated Reasoning about System designs


Starting date of the position: as soon as possible.

DESCRIPTION

The development of complex hard- and software systems is error-prone and costly. One technique that can provide very valuable feedback on the correctness of system designs is model checking. It involves exhaustively analysing a system design to determine whether it satisfies desirable functional properties. However, it is computationally very demanding.

The GEARS project is led by dr.ing. Anton Wijs. At the TU/e, he develops model checking techniques that are accelerated by the use of graphics processing units (GPUs). GPUs offer great potential for parallel computation, while keeping power consumption low. However, not all types of computation can trivially be performed on GPUs, sometimes the algorithms need to be entirely redesigned. Currently, he has an explicit-state model checker, called GPUexplore, that can run hundreds of times faster than conventional model checking approaches.

Regarding symbolic model checking techniques, IC3 is currently state-of-the-art; it can analyse large designs in reasonable time, but its limitations still mean that it is not used very commonly for the design of systems today. IC3 uses SAT solving, or the solving of Boolean or propositional satisfiability problems, as a subroutine.

In the GEARS project, the candidate will investigate whether GPUs can be employed for IC3. First of all, the candidate will investigate how SAT solving can be accelerated using GPUs, specifically focussing on SAT problems that stem from model checking. Second of all, (s)he will investigate how IC3 can benefit from using GPUs. IC3 is reportedly parallelisable, but how GPUs can be used to do so most effectively is still an open question.

The project potentially has an enormous impact, since IC3 is currently state-of-the-art in symbolic model checking, and SAT solving is used not only for model checking, but in many different application domains.

The research will be conducted in the Model Driven Software Engineering section of the Computer Science department at TU/e. This section consists of two research groups, Formal System Analysis (FSA) and Software Engineering and Technology (SET). The FSA group studies techniques to model and analyse discrete system behaviour in a mathematically rigorous way, while the SET group develops methods and tools for time- and cost-efficient evolution of high-quality software systems.

REQUIREMENTS

We are looking for candidates that meet the following requirements:

- MSc in Computer Science;
- Experience in, and enthusiasm for, programming (not necessarily parallel programming);
- Good communicative skills in English, both in speaking and writing. Candidates should be prepared to prove their English language skills.

Besides the above requirements, the candidate should also fit at least one of the two following profiles:

1. The candidate has knowledge of formal verification and experience in the involved algorithms, and is interested in programming GPU applications to speed up model checking. This includes having an interest in learning about the hardware characteristics of GPUs, and how to optimise applications that run on them.

2. The candidate has knowledge of parallel programming / high performance computing (not necessarily GPU programming in particular), and is interested in learning about formal verification. This includes learning the theory of model checking and SAT solving. At TU/e, the MDSE section provides courses on these topics that can be attended by the candidate.

Candidates that fit both profiles are particularly encouraged to apply.

WORKING CONDITIONS:

We offer:
• full-time employment as a PhD-candidate for a period of 4 years;
• a gross salary of € 2.191 per month in the first year increasing up to €2.801 in the fourth year;
• annually 8% holiday allowance and 8.3% end of year allowance;
• support with your personal development and career planning including courses, summer schools, conference visits etc.;
• a broad package of fringe benefits (including an excellent technical infrastructure, child care, moving expenses, savings schemes, coverage of costs of publishing the dissertation and excellent sports facilities).

INFORMATION AND APPLYING

For more information about the project, please contact dr.ing. Anton Wijs, e-mail: A.J.Wijs@tue.nl<mailto:A.J.Wijs@tue.nl>

For information about employment conditions, please contact Pim Hertogs LLM MSc (HR advisor), e-mail: pzwin@tue.nl<mailto:pzwin@tue.nl>

The application should consist of the following parts:
• a motivation letter;
• a Curriculum Vitae;
• copies of your diplomas together with the list of grades, and other relevant certificates;
• names and addresses of two referees;
• proof of English language skills (if applicable);
• a 2-page research statement about the project topics.

Please apply by submitting the above documents via this website:
http://jobs.tue.nl/en/vacancy/phd-position-project-gears-311483.html
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************