The research activities of the Hycomes team can be separated into four topics, as listed below:
- Multimode DAEs, used for the modeling of large-scale physical systems and Cyber-Physical Systems, are not handled in general by the existing tools. Our research aims at addressing their correct simulation as well as providing theoretical results on the existence and uniqueness of solutions.
- Contract-based design emerged in the early 90’s as a needed formalization of the principles of requirement engineering, and extensions to Cyber-Physical Systems are being developed since the 2000’s. Our works, in the context of an international collaboration, led to the design of a contract meta-theory that offers possibilities far beyond the current practical use of contracts.
- Formal verification:
- Computer Algebra (or symbolic computation) is the main pillar behind the formal verification of dynamical and hybrid systems. The algebraic characterization of positively invariant sets is crucial to discharging proof obligations for such systems in any proof assistant.
- Boolean Functions and their representation are known to be a key concern in circuit design and formal verification (among others); our works also give them an essential role in the study of multimode DAEs. Models and data structures that reduce the computational costs for representing and computing on Boolean functions are studied.
- Probabilistic modeling and programming is at the core of the study of graphical models, whose applications range from Bayesian statistics to machine learning and arise in biology, computer vision and other fields. Our works propose a new model of mixed automata that generalizes probabilistic graphical models.
A summary of our results, extracted from our latest annual activity report, is also available.