Reachability analysis is a major problem in the verification of hybrid systems. Set integration and abstract interpretation approaches can be seen as complementary and their combination has the potential to significantly improve the efficiency of verification algorithms. This PhD thesis aims at studying and developing new abstract domains for both continuous and discrete variables in a hybrid system. The thesis is funded within the ANR project MALTHY (Jan 2014 - Jan 2018) which focuses on advancing the state of the art in real-time and hybrid model checking by employing advanced methods and tools from the mathematical sciences of algebra and geometry.
Research will take place at the VERIMAG laboratory in Grenoble, France (3 years). VERIMAG is a joint research laboratory of Université Joseph Fourier (UJF) and CNRS (French National Center for Scientific Research). The term of the PhD funding is 3 years.
The selected applicant will be registered as PhD student at UJF and the thesis will be co-advised by Thao Dang (CNRS researcher and the Principal Investigator of the project MALTHY) and Vasiliki Sfyrla (a research scientist at Object Direct).
