(a) The interplay between static analysis and model checking;
(b) Methods and techniques for the analysis of discrete or stochastic features;
We are interested both in candidates aiming to perform foundational work and those that are interested in studying how to analyse concrete applications. We often describe our models using appropriate process calculi or suitable automata; similarly properties are often described in logics such as Alternation- free Least Fixed Point Logic, Computation Tree Logic, Continuous time Stochastic Logic or variants of these.
Static analysis techniques incorporate Abstract Interpretation, Flow Logic, Type and Effect Systems; model checking incorporates discrete and stochastic model checking.
http://www.dtu.dk/English/About_DTU/vacancies.aspx?guid=66ed37e6-4889-4eff-8e60-6c37e85e8540
Please quote 10 Academic Resources Daily in your application to this opportunity!
