Action experts will participate in a number of activities sponsored by national and EU projects (see Section B.4). Through its experts, the Action will therefore actively interact with the related domain-specific research. The experts will regularly present research finding from the application areas at the Work Group meetings and communicate the relevant benchmarks.
As a specific example of the nature of this interaction, we point out the simultaneous synergy and non-overlap with the area of software verification. A number of software verification tools focus on rich programming language constructs and programming methodology, such as object-oriented methodology, but use automated reasoning techniques as a black box, without developing automated reasoning techniques themselves. The proposed Action develops such automated reasoning techniques, taking into account the needs of several application domains. The results of the Action will therefore eliminate the bottlenecks currently experienced by software verification tools, especially in the area of verifying strong properties that ensure correct functioning of software.
However, in addition to software verification, important application domains of the Action include hardware verification and synthesis, formalized mathematics, reasoning about medical terminologies, and the semantic web. Each of these areas has its own community of researchers, and a strong economic dimension of its own. What is common to all of them is the need for automated reasoning expertise. The unification of such expertise across different application domains is one of the justifications for the present Action.