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.