The Action will advance algorithms and implementations of automated reasoning technology, making them applicable to a wider range of tasks in the design and implementation of computer systems. The focus of research includes the following example topics as well as the topics that are naturally connected or build on them:
- new specialized algorithms, not be limited by any particular application area, as long as the underlying rich model has the mathematical structure supported by the algorithm;
- techniques that compose multiple specialized algorithms into algorithms applicable to a wider range of problems, with understood guarantees on the soundness, completeness, and efficiency;
- Rich Model Language design that takes into account the ease of modelling, current specialized languages, requirements of existing and new algorithms and tools, and interactive theorem proving language semantics;
- the adaptation of existing tools and the development of new tools that support Rich Model Language, including both tools for automated reasoning about Rich Models (including deduction, analysis and synthesis), and tools for automatically generating Rich Models;
- computer experiments with automated reasoning about rich models from the area of software, hardware, embedded, and information system verification.
The pace of the activities will crucially depend on the ability to develop and share the expertise among Action participants. The research (and dissemination) activities will be carried out by researchers using state-of-the art commodity computing equipment (desktops, compute servers, web servers).
The research will be carried out in at least the following cross-cutting and collaborating Work Groups:
- Rich Model Language: Design and Benchmark Suite
- Decision Procedures for Rich Model Language Fragments
- Analysis of Executable Rich Models
- Synthesis from Rich Model Language Descriptions