The Action will achieve its objectives through the development of foundations and tools of the Rich-Model Toolkit infrastructure. The infrastructure will consist of a collection of Rich Models, and a system of tools communicating using the Rich Model Language. The work will be structured according to the following four initially-envisioned Work Groups.

Rich Model Language and Benchmarks written in this language are among concrete results and unifying themes of the Action, and are the subject of Work Group 1. The activities of Work Group 1 will include:

1. Rich-Model Language design, including abstract and concrete syntax, as well as semantics; inspired by the expressiveness of provers such as Isabelle/HOL while aiming for simplicity of automated processing present in more specialized languages;
2. translations between Rich Model Language and languages such as Isabelle/HOL, SMT-LIB, TPTP, and OWL;
3. design of formats for expressing manually and automatically constructed proofs and counterexamples for properties of Rich-Models, as well as implementing efficient and trustworthy checkers and visualizers for these formats;
4. Rich Model benchmark collection for comparing different tools and measuring progress in tool development, made publicly available on the Web
5. helping adapt existing design, analysis, and synthesis tools to take advantage of Rich Model infrastructure
6. realistic plans for running Rich Model tool competition

The tools in Rich-Model Toolkit will accept a set of Rich Models and produce a new set of Rich Models (with output in a formally verifiable relationship to the input). This general view supports not only the traditional validity and satisfiability checking, but also optimization and synthesis problems.

The Action will build on the experience from the following past successes of its experts

1. initiating successful community standards for automated reasoning tools
2. leading major efforts in proof-assistant development
3. developing specialized automated reasoning tools
4. automated generation of models from applications such as hardware and software verification.

The Action is therefore in a unique position to develop Rich Model Language format and to advertise it within the scientific community, which in turn will foster the adoption of similar formats in industry.

Work Group 2 focuses on automating the reasoning about Rich Models through development, analysis, implementation, formal verification, and applications of decision procedures. A decision procedure typically accepts a class of rich models representing logical formulas and (within well-understood time and space bounds) provides an answer about the validity of the formula. Decision procedures of interest in the Work Group include decision procedures for sets, collections with cardinality bounds, relations, arrays, bit vectors, transitive closure logics, non-linear arithmetic, and description logics. Among the topics of interest are the following.

1. the improvement of efficiency of existing decision procedures
2. the development of new decision procedures
3. integration of decision procedures into satisfiability modulo theory (SMT) and resolution frameworks
4. automated synthesis of decision procedures, in collaboration with Work Group 4
5. modular, flexible, and efficient implementations of SAT and SMT solvers, including
   • proving validity of Rich Models
   • finding counterexamples
   • solving optimization problems
   • supporting the use of off-the-shelf SAT/SMT solvers through converters between the Rich-Model Language and standard DIMACS and SMT-LIB input formats
   • extensible SMT solver architectures that support multiple background theories (such as Nelson-Oppen and DPLL(T1,…,Tn) combination)
   • efficiency improvements in SMT and SAT, including non-clausal solvers
6. applications of SAT and SMT solving to real-world decision and optimization problems, including
   • hardware verification
   • software verification
   • planning of industrial processes
   • nurse scheduling
   • sport timetabling
7. improving techniques for encoding real-world problems into SAT and SMT, including
   • design and implementation of high-level Rich Model Language support that enables natural problem description while leaving space for efficient choice of encoding
   • choosing appropriate background axioms and controlling quantifier instantiation
   • automation of the encoding process starting from high-level Rich Models
8. formal verification of decision procedures, enabling their use as a part of larger mission-critical software
   • extending solvers to generate evidence (models for satisfiable formulas and proofs for unsatisfiable formulas) in Rich Model infrastructure
   • applying software verification techniques to verify the calculi and entire implementations of SAT and SMT solvers
   • development of verified implementations of quantifier-elimination procedures
   • the role of synthesis in obtaining provably correct decision procedures
9. scalable reasoning in expressive description logics with applications to
   • medical ontologies (SNOMED, NPfIT, GALEN, NCI Thesaurus, OBO Foundry)
   • software systems
   • Semantic Web, e-Science, and the Grid.

Through these activities Work Group 2 will contribute to the development of formally verified and efficient automated reasoners for a significant class of practically relevant Rich Models.

Work Group 3 focuses on the analysis of dynamic changes in systems such as software systems, hardware designs, embedded systems, and communication protocols. Such changes can be described by a general notion of a transition system. Transition systems are therefore an important class of rich models, with both exact semantics and a mapping to physical implementations. To address the decidability and complexity limitations of the general problem, Work Group 3 focuses on

1. abstraction-based approaches that provide semi-algorithms for the general analysis tasks
2. efficient algorithms for the specialized subclasses.

Properties considered include both safety (reachability) and liveness (termination). The group aims to develop theory, algorithms and implementations for verification of transition systems by leveraging the expertise across the areas of abstract interpretation, automated deduction, and constraint solving. Specific subproblems considered include the following.

1. developing new abstraction refinement techniques, which play a crucial role for the analysis of systems with looping (cyclic) control-flow structures, including, including
   • developing refinement techniques and tools that deal with expressive data types such as lists, trees, and their combination with arithmetic
2. developing abstraction-based analysis techniques and tools suitable for finding both proofs and witnesses for property violation
3. combining precise (but potentially slow) predicate abstraction techniques with fast (but potentially imprecise) specialized analyses to reduce the number of abstraction refinement iterations and speed-up the analysis
4. exploring synergy between synthesis methods in Work Group 3 and the invariant/ranking function generation techniques used for transition system analysis. This ambitious direction will exploit the duality of synthesis and analysis to deliver better theoretical insight and automatic tool support for both tasks
5. integration of data-flow analysis algorithms, shape analyses, SAT, SMT and BDD-based model checkers into the Rich Model framework
6. symbolic execution and bounded model checking on rich models
7. integration of state/event-based formalism into Rich Models
8. integration of transition system analysis and SMT solver technology of Work Group 2 to improve overall search efficiency.
9. developing tools that extract Rich Models from software source code, software bytecode, and hardware designs, with applications such as
   • automated analysis of deep properties of functional programs
   • analysis of linked and concurrent data structure implementations
   • scalable analysis of correct resource use and related finite state protocols
   • automated detection of security flaws, attacks, intrusions, and violations of user-specified policies.

Through a combination of tools that extract Rich Models and tools that analyze rich models, Work Group 3 will enable automated analysis of expressive properties of computer systems.

Work Group 4 explores the theory, tools, and usability of synthesis in system development. In contrast to automated verification algorithms that establish whether a given system satisfies a given specification, synthesis algorithms automatically construct the implementation that is guaranteed to satisfy a given specification. Synthesis is more difficult than verification, and is one of the holy grails of Computer Science. Despite impressive theoretical results of the past, it was only recently that researchers made significant steps towards the development of practical synthesis algorithms. Synthesis still has many limitations preventing its wider practical application. Work Group 4 aims to address these limitations through tasks that include the following.

1. developing synthesis algorithms for more expressive logics, including
   • identifying decidability and worst-case complexity of synthesis for rich logics
   • developing heuristics and new subclasses of problems that overcome high complexity
   • lifting decision problems (explored in Work Group 2) to synthesis problems
   • developing high-level synthesis techniques applicable to components
   • synthesis of hybrid systems
2. efficient implementations of synthesis algorithms using not only binary decision diagrams but also quantified (Boolean) formulas
   • developing benchmarks for synthesis problems within the Rich Model benchmark suite from Work Group 1
3. quantitative generalization of synthesis
   • extending Boolean specifications by quantitative measures in order to rank implementations by laziness, fairness, or parsimonious use of resources
   • non-boolean algorithms that generalize decision procedures from Work Group 2
   • quantitative games as a method for solving synthesis problems
4. simplified synthesis problems of practical interest, including
   • problems with limited quantifier alternations
   • using synthesis for repair and sketching
5. the use of synthesis to implement very-high-level programming language constructs.

Action experts have a unique set of complementary skills, whose combination will be necessary to fulfill the research vision of synthesis. By giving a more active role to automated tasks and avoiding low-level coding, synthesis has the potential to dramatically improve the productivity of computer system developers.