The Action coordinates activities on developing infrastructures for automated reasoning about Rich Models of computer systems. Rich Models have the expressive power of a large fragment of formalizable mathematics, enabling specification of software, hardware, embedded, and distributed systems. Rich Models support modeling at a wide range of abstraction levels, from knowledge bases and system architecture, to software source code and detailed hardware design.

The Action contributes to the construction of Rich-Model Toolkit, an infrastructure that precisely defines the meaning of Rich Models and introduces standardized representation formats and incorporates a number of automated reasoning tools. Moreover, the Action develops and deploys new tools for automated reasoning that communicate using these standardized formats. The resulting tools will have a wide range of applicability and improved efficiency, helping system developers construct reliable systems through automated reasoning, analysis, and synthesis.

automated reasoning, automated theorem prover, decision procedure, verification, synthesis