Position: Post-doc at Laboratory VERIMAG and INRIA POP-ART Project
Location: Laboratory VERIMAG and INRIA POP-ART Project Context: the post-doc position is opened within the ANR funded project VEDECY (Verification of Cyber-Physical Systems). The project brings together researchers from the Laboratory Verimag, the INRIA POP ART Team, and the Laboratory Jean Kuntzmann (http://sites.google.com/site/vedecy/). It aims at pursuing fundamental research towards the development of algorithmic approaches to verification and design of cyber-physical systems.
Position Description: An important problem we want to tackle in the project is the verification of embedded control software (with complex discrete dynamics) that interacts with a physical system. Almost all approaches for verification of hybrid systems assume a simple discrete dynamics on a simple, typically finite, state-space.
In this post-doc, we focus on embedded control programs specified using the language LUSTRE. and consider the following problems:
1. Studying variants of « widening » operator (commonly used in program verification) that is appropriate for the unbounded-time analysis of discrete-time hybrid automata with linear dynamics. One idea is to exploit properties of differential equations.
2. Template polyhedra are set representations that can efficiently approximate the set of all trajectories of a hybrid automaton. The arising question is to infer the relevant template expressions that will lead to precise results with respect to a specific verification problem.
3. Another direction involves the use of affine forms or zonotopes, which can yield more precise results than convex polyhedra for many non-linear operations.
4. For these questions regarding numerical behaviours, a common issue is the combination with the discrete/Boolean behaviour induced by the control software (typically a LUSTRE program).
5. Implementation of the theoretical results in a toolbox for verification of systems combining LUSTRE programs and hybrid automata
- Requirements* The successful candidate should have a Ph.D. in Computer Science, Automatic Control, Applied Mathematics. Knowledge of formal verification and related areas is a plus. Programming experience (ideally C, C++, OCaml) is required.