Better Synthesis for Underspecified Quantitative Systems – BisoUS

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.