CE48 - Fondements du numérique : informatique, automatique, traitement du signal

Better Synthesis for Underspecified Quantitative Systems – BisoUS

Submission summary

Computer systems are ubiquitous and identifying their possible defects is crucial already at the earliest stages of their development, when many aspects, including the environments or the execution platforms, have not been fixed. Verification must then be performed on underspecified models and, somehow inconsistently, should give answers as understandable as possible.

In this project, we aim at developing verification techniques for underspecified models that take this explainability constraint into account, by optimizing resources, such as energy or memory, and synthesizing more precise requirements on the underspecified aspects of the models under which the system behaves correctly.

We depart from classical formalisms and consider their combined extensions with three complementary ingredients: costs/rewards for resource consumption; parameters for unknown quantitative characteristics; and games for representing all the behaviours of the underspecified system.

The main problem with the highly expressive formalisms we want to study and promote is that the associated verification and synthesis problems are very complex, in the algorithmic sense, resulting in processor and memory usage that is prohibitive in practice. Moreover, the related decision problems are most often undecidable.

To address this problem, we follow two complementary approaches. On the one hand, and this is the most often explored approach for this type of situation, we identify subclasses of the general formalism that model well certain targeted applications and for which we believe we can obtain better theoretical and practical results.

On the other hand, we propose the development of specific algorithms operating on the general formalism but giving approximated results, together with formal guarantees on the approxmation realized.

Project coordination

didier lime (Ecole Centrale de Nantes)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.


IRISA Institut de Recherche en Informatique et Systèmes Aléatoires
LIPN Université Sorbonne Paris Nord (Paris 13)
LS2N Ecole Centrale de Nantes
LMF UPSaclay - Laboratoire Méthodes Formelles

Help of the ANR 409,023 euros
Beginning and duration of the scientific project: March 2023 - 48 Months

Useful links

Explorez notre base de projets financés



ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter