Applications will be evaluated on a monthly basis. The vacancy may be closed early once the positions are filled.
We offer two Ph.D. positions within the TruSTy project on “Trustworthy Analysis of Stochastic Timed Systems” funded by NWO, the Dutch Research Council. The project’s goal is to create new highly-reliable approaches – languages, algorithms, and tools – for the modelling and analysis of complex systems subject to uncertainty. The project’s mathematical foundations are extensions of continuous-time Markov chains and Markov decision processes. Its approach is the development of sound, fast, and provably correct algorithms with the assistance of interactive theorem provers.
As Ph.D. student on TruSTy, you will develop new approaches for sound probabilistic model checking (typically based on numeric fixpoint algorithms and implemented via floating-point arithmetic with carefully managed rounding) or statistical model checking (exploiting and extending the decades of research in statistics for application in our domain). You will carefully balance algorithm performance and scalability with numeric accuracy requirements. To prove the correctness of your algorithms, you can use the Isabelle interactive theorem prover; with the Isabelle Refinement Framework, you can turn your proofs into high-performance and correct-by-construction executable LLVM bytecode. The results of your research will be integrated into the Modest Toolset, a comprehensive suite of quantitative verification tools developed and maintained by the TruSTy team since 2008.
Your work will be guided and supervised by senior researchers that are experts in probabilistic and statistical model checking (Arnd Hartmanns) and interactive theorem proving (Peter Lammich). You will have the opportunity to work together
- Formal methods, verification, and model checking
- Interactive theorem proving
- Algorithms and data structures
- Probability theory and statistics
Are you interested in this position? Please send your application via the 'Apply now' button below, and include:
Applications will be evaluated on a monthly basis. The vacancy may be closed early once the positions are filled.
The Formal Methods and Tools group is part of the Computer Science department of the University of Twente. Our mission is to develop mathematical methods, high-performance data structures and algorithms, and suitable programming languages for the design of reliable software- and data-intensive control systems.
The group consists of approximately 40 researchers with a very diverse background. We have an open and inclusive atmosphere, with many group activities (both work-related and fun).
The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.
Looking for a job that matters? Join the university of technology that puts people first – and shape new opportunities both for yourself and for ou...
De pagina van de werkgever bekijken