Abstract
Maria Paola Bonacina
Title: Conflict-Driven First-Order Decision Procedures
Abstract: Conflict-driven decision procedures for SAT and SMT search simultaneously for a model or a refutation of the input formula by building candidate models, deriving new formulae implied by the input, detecting conflicts between model and formulae, and repairing the model by conflict-driven inferences. A current research direction in automated reasoning generalizes this notion of conflict-driven satisfiability to a paradigm of conflict-driven reasoning also at the first-order level. This talk sketches the landscape of these developments, and then focuses on SGGS (Semantically-Guided Goal-Sensitive reasoning) which is a conflict-driven first-order theorem-proving method. SGGS is attractive as a basis for decision procedures, because it is refutationally complete and model complete in the limit, which means that if it halts detecting satisfiability, it gives a model. This talk covers results showing that SGGS decides known (e.g., EPR) and new decidable fragments of first-order logic, but not other known decidable fragments. SGGS is implemented in a new theorem prover named Koala.
(SGGS is joint work with David A. Plaisted; SGGS decision procedures and Koala are joint work with Sarah Winkler)
Philipp Rümmer
Title: Solving String Constraints, Starting From the Beginning and From the End
Abstract: The recent years have seen a wealth of research on string solvers, i.e., SMT solvers that can check satisfiability of quantifier-free formulas over a background theory of strings and regular expressions. String solvers can be applied in different verification algorithms, for instance in symbolic execution to check path feasibility, in software model checking to take care of implication checks; a prime application area is security analysis for languages like JavaScript and PHP, for instance to discover vulnerability to injection attacks. To process constraints from those domains, it is necessary for string solvers to handle a delicate combination of (theoretically and practically) challenging operations: concatenation in word equations, to model assignments in programs; regular expressions or context-free grammars, to model properties or attack patterns; string length, to express string manipulation in programs; transduction, to express sanitisation, escape operations, and replacement operations in strings; and others. This talk will give a general introduction to string solving, and then present a solver architecture based on the concept of pre-image computation that is simple, yet turns out to be complete for an expressive fragment of string constraints. The architecture has been implemented in our solver OSTRICH (and is the result of joint work with many people).