[isabelle] PhD Position at Eindhoven University of Technology

The Eindhoven University of Technology invites applications for a PhD position funded by the Dutch National Science Foundation (NWO) under the project “Formal Cache Coherence Verification of Multi-Core Architectures”. The position is for 4 years. The project must start no later than 1 November 2014.

The deadline for applications is September 1st. Applications will be considered until the position is filled.

Project Summary

This project is about developing theories and tools for the formal verification of detailed micro-architectural models of multi-core architectures. The main objective is to support the verification of cache coherence. The project theoretical aspects are concerned with developing a general theory of cache coherence architectures in theorem proving systems (e.g. ACL2, Isabelle/HOL) and explore how this system level property can be decomposed into smaller and component level properties. The practical aspects are concerned with developing new verification algorithms for, e.g., reachability, message orderings, equivalence, for large and detailed models.

This project involves close collaborations with Intel Strategic CAD Labs in Portland (USA) and STMicroelectronics in Grenoble (France).


We are looking for candidates with an Msc degree — or equivalent — in computer science, mathematics, electrical engineering, or a closely related field. A solid theoretical background with the desire and skill to let the research have practical impact. The working language is English. Applicants are expected to have good communication skills and the ability to work in teams.

Appointment and Salary

We offer a challenging job in a dynamic and ambitious university and a stimulation research environment. The Eindhoven University of Technology also provides an extensive package of fringe benefits (e.g. excellent technical infrastructure, the possibility of child care and excellent sports facilities).

Salary initially starts at 2.083 Euro’s per month and ends at 2.664 Euro’s per month, with an 8% bonus for vacations and a 13th month. Applicants coming from outside the Netherlands may qualify for a special 30% rule, where 30% of the growth income is tax free. Salary may be adjusted depending on your experience.


The research will be conducted in the research group Formal System Analysis of the Mathematics and Computer Science department. The FSA group is concerned with modelling and formally verifying system behaviour, either by employing process equivalences, modal formulas or behavioural reduction and visual inspection. Lately, a lot of interest goes into parameterized boolean equation systems, especially employing the power of SMT solvers and other symbolic reduction techniques.


For information about this position, please contact Julien Schmaltz per email (j.schmaltz at tue.nl<mailto:j.schmaltz at tue.nl>) or per phone +31 40 247 8691.


The application should consist of a cover letter explaining your motivation and qualifications for this position, a detailed Curriculum Vitae including a list of publications, and contact information of two references. Please send your application before September 1st 2014 to j.schmaltz at tue.nl<mailto:j.schmaltz at tue.nl>.

Dr. Julien Schmaltz
Eindhoven University of Technology
Department of Computer Science
Model Driven Software Engineering
Formal System Analysis
Room MF7.071b
Postbus 513 5600 MB Eindhoven
j.schmaltz at tue.nl<mailto:j.schmaltz at tue.nl>
Tel.: +31 40 247 8691
Fax: +31 24 246 8508

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.