This section reviews current state of knowledge in automated reasoning according to the type of the reasoning technique. It concludes with an overview of related standardization efforts that have made such techniques more widely applicable.

**SAT solvers**, such as zChaff, Berkmin, and Minisat, solve
the satisfiability problem for propositional logic. They
made great progress in the past decade, showing that
worst-case computational complexity does not prevent
practical applications of tools in verification of hardware
and software, and invigorated research in automated
reasoning about more expressive classes of problems.

**Finite model finders**, such as Paradox and Kodkod, search
for finite structures that satisfy given first-order logic
formulas, often based on a reduction to SAT. They proved
very useful in finding counterexample to conjectures,
including those that involve properties of software
implementations and designs.

**First-order theorem provers** find proofs of validity of
given first-order logic formulas (in contrast to model
finders that find counterexamples). Decades of research
into variants of resolution resulted in implementations such
as SPASS, E, and Vampire, that are very effective at proving
a wide range of valid first-order logic formulas. Promising
areas of research are methods that combine proof search and
model finding, improving the effectiveness of both
approaches.

**Description logics** overcome the undecidability of
first-order logic by adopting a form of bounded quantifiers.
Reasoning tools based on decidable description logics, such
as FaCT++, Racer, and Hermit, have proved capable of
handling complex formulas while scaling to problem instances
with a large number of background axioms. Such progress was
made possible by systematic study of decidability,
complexity, and practical reasoning algorithms for specific
classes of formulas.

**Decision procedures** of practical importance also include
the MONA tool for weak monadic second-order logic over
trees, which found important applications such as
verification of linked data structures. Also relevant are
arithmetic decision procedures and procedures for reasoning
about sets and multisets, which have incorporated insights
from linear programming. Such specialized reasoning
techniques have recently seen both theoretical advances and
implementations in the context of more general reasoning
systems.

**Satisfiability modulo theories** (SMT) is among such
reasoning techniques that show great promise in combining
multiple decision procedures into a decision procedure for a
richer language. SMT solvers build on techniques such as
Nelson-Oppen combination of disjoint theories, and have
recently seen significant advances in the context of
SAT-based frameworks such as DPLL(T), and successful
standardization activities such as the SMT-LIB initiative.

**Hardware and software verification** has benefited from
the advances in SMT reasoning, and helped identify the area
of reasoning about transition systems. Just as in reasoning
about first-order formulas, we can distinguish model finding
methods, such as bounded-exhaustive testing and explicit
state model checking, and proof-based methods. The success
of automated reasoning about safety and liveness of
finite-state systems is witnessed in routine use of these
techniques by major microprocessor manufacturers,
acknowledged by the most recent Turing award. Recently,
techniques based on predicate abstraction, bounded model
checking, transition invariants, and symbolic shape analysis
brought together research in transition systems and research
in decision procedures for formulas, resulting in tools for
automated analysis of infinite-state transition systems.

**Abstract interpretation** is a related techniques for
analyzing infinite-state systems. Abstract interpretation
tools have recently seen great successes, such as the use of
ASTREE and Absint tools in the analysis of avionics
software. Such analyzers are based on parameterized
abstractions and have recently made use of advances in
decidable classes of logical constraints, such as difference
logics. Among the goals of the Action is taking further
such fruitful combinations and identifying similar
cross-fertilization opportunities between other sub-fields
of automated reasoning.

**Automated synthesis** of executable systems from
specifications techniques is among the most ambitious
approaches to reliable computer systems. Most of the above
automated reasoning tools can provide not only simple yes/no
answers but also concrete counterexamples, proofs, and
reachability invariants. An active area of research is
productively exploiting such information for constructing
reliable computer systems. Recent exciting practical
applications include specialized software synthesis
approaches and hardware synthesis from linear temporal logic
specifications.

**Standardization activities, benchmarks, and competitions**
have tremendously accelerated the development of automated
reasoning tools.

- TPTP formats for first-order logic that have long provided stable interfaces to powerful provers.
- DIMACS format for SAT, with the SAT Competition and the SAT Race is often credited with sparking great advances in SAT solving.
- The SMT-LIB initiative defined standard input/output formats and interfaces to SMT solvers. Over a period of several years it became supported by a number of SMT solvers, and a number of formal methods client applications. The initiative runs an influential yearly competition, SMT-COMP, and contains a growing repository of over 40,000 benchmarks from academia and industry.

Such standardized formats will become even more successful if they support natural descriptions of a wider range of problems. The starting point for the Rich Model language designed as part of the Action are therefore the expressive languages of interactive provers such as Isabelle, HOL, and Coq. On the syntactic side, related initiatives include OMDoc, whose goal is the representation of mathematics on the Web. However, the key property of concrete interactive theorem provers languages is their clear and well-understood semantics, as well as the number of defined concepts from computer science and mathematics contained in their libraries. The adequacy of these library definitions is empirically proven through formalizations such as the correctness proofs for Java infrastructure, correctness of SAT solvers, metatheorems of first-order logic, deep results in set theory, the proof of four-color theorem in graph theory, and proofs of important steps of the Kepler conjecture. The process of formalizations continues through new submissions to the Archive of Formal Proofs (http://afp.sourceforce.net) and efforts such as the Verisoft project and the POPLmark challenge. In the area of the transition system analysis, the conference on Computer-Aided Verification recently introduced a competition for hardware verification with a standardized input format. In the area of software, intermediate formats with precise semantics include SAL from SRI and BoogiePL from Microsoft Research.

Innovative activities of the Action include all areas summarized in this section. They involve theoretical work on decidability, complexity, and algorithm design, as well as tool development and computing experiments on models of practical interest. Overall, they contribute to wider applicability of automated reasoning about computer systems.