Internship | ADA Software Model Checking

Do you believe in formal methods? This is your opportunity to show their benefits for the high-tech industry.



Education type

university (wo)


Internship and graduation project

Hours a week

Fulltime – 40


Apply now


What will you be doing?

Nexperia’s Equipment & Automation Technologies (E&A) department develops pick-and-place machines for the production of semiconductor products, such as transistors, diodes and ICs. The Bright project is a cooperation of Nexperia and ESI (TNO) addressing model-based systems engineering with Nexperia’s pick-and-place machines as the carrying industrial case.

One of the topics of the Bright project is modelling and analysis of the software of the pick-and-place machines. This software involves distributed control software implemented in the ADA programming language. The control and coordination of the software’s parallel processes is realised using signals and locks. The code’s parallelism make it difficult to verify and validate all possible control flows, e.g. for deadlocks/livelocks.

The Bright project aims at formal verification and validation of the software. This student assignment targets a formal verification of the software’s control and coordination flow using Nexperia’ ADA codebase as a starting point. The aim is to develop a methodology to (1) automatically derive a formal model from the code and (2) apply model checking to the derived model, e.g. to prove the absence/existence of deadlocks/livelocks in the control and coordination flow.

The formal model can be derived from the code using execution traces and available tools, such as parsers creating Abstract Syntax Trees (ASTs). By appropriately filtering and combining ASTs, the relevant parts of the code are captured in the model, while less important parts are eliminated.
Ideally, the methodology to be developed includes automatic traceability from the derived formal model back to the code. This would allow Nexperia’s software developers to relate found issues, if any, back to their code base.

What do we require of you?

You are an MSc student Computer Science looking for a graduation assignment of 6-9 months. You have experience with formal methods and preferably static analysis. You think it is a challenge to work in a multi-disciplinary environment and like your graduation assignment to show the benefits of scientific system development methods in a high-tech organisation.

What can you expect of your work situation?

TNO is an independent research organisation whose expertise and research make an important contribution to the competitiveness of companies and organisations, to the economy and to the quality of society as a whole. Innovation with purpose is what TNO stands for. With 3000 people we develop knowledge not for its own sake but for practical application. To create new products that make life more pleasant and valuable and help companies innovate. To find creative answers to the questions posed by society. We work for a variety of customers: governments, companies, service providers and non-governmental organisations. Working together on new knowledge, better products and clear recommendations for policy and processes. In everything we do, impact is the key. Our product and process innovations and recommendations are only worth something if our customers can use them to boost their competitiveness.

The assignment will be carried out at Nexperia’s E&A department in Nijmegen under supervision of ESI (TNO) and Nexperia.

What can TNO offer you?

You want to work on the precursor of your career; a work placement gives you an opportunity to take a good look at your prospective future employer. TNO goes a step further. It’s not just looking that interests us; you and your knowledge are essential to our innovation. That’s why we attach a great deal of value to your personal and professional development. You will, of course, be properly supervised during your work placement and be given the scope for you to get the best out of yourself. Naturally, we provide suitable work placement compensation.

Has this vacancy sparked your interest?

Then please feel free to apply on this vacancy! For further questions don’t hesitate to contact us.

Contact: Jacques Verriet
Phone number: +31 (0)88-86 65468

Note that applications via email and third party applications are not taken into consideration.


Apply now



Stay up to date with our latest news, activities and vacancies collects and processes data in accordance with the applicable privacy regulations for an optimal user experience and marketing practices.
This data can easily be removed from your temporary profile page at any time.
You can also view our privacy statement or cookie statement.