ABSTRACT. (joint work with M. Echenim and S. Tourret)

Abstract: Abduction can be defined as the process of inferring plausible explanations (or hypotheses) from observed facts (conclusions). This form of reasoning has the potential of playing a central role in system verification, particularly for identifying bugs and providing hints to correct them. We describe an approach to perform abductive reasoning that is based on the superposition calculus. The formulas we consider are sets of first-order clauses with equality, and the abducibles (in other words the hypotheses that are allowed to be inferred) are boolean combinations of equations constructed over a given finite set of ground terms. By duality, abduction can be reduced to a consequence-finding problem. We thus show how the inference rules of the superposition calculus can be adapted to obtain a calculus that is deductive complete for ground clauses built on the considered sets of ground terms, thus guaranteeing that all abducible formulas can be generated. This calculus enjoys the same termination properties as the superposition calculus: in particular, it is terminating on ground extensions of decidable theories of interest in software verification.

The number of implicates of a given equational formula is usually huge. We describe techniques for storing sets of abduced clauses efficiently, and show how usual trie-based approaches for representing sets of propositional clauses in a compact way can be adapted and extended in order to denote equational clauses up to equivalence (modulo the axioms of equality). We provide algorithms for performing redundancy pruning in an efficient way on such representations. We identify hints for improvements and provide lines of on-going and future research.

ABSTRACT. The Nelson-Oppen combination method is ubiquitous in all Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories connected via bridging functions. This problem is of greatest interest for solving verification problems expressed in a combination of data structures and arithmetic. Our work can be viewed as a synthesis of previous contributions by different authors, based on different techniques and frameworks, like the one developed by Sofronie-Stokkermans based on locality principles. We investigate here an approach by reduction from non-disjoint to disjoint combination which is particularly well-suited to combine a wide range of data structures with bridging functions over a target theory. We focus on data structures for which the standard superposition calculus provides an off-the-shelf underlying satisfiability procedure. We also consider the problem of adapting the combination procedure to get a satisfiability procedure for a standard interpretation of the data structure.

ABSTRACT. Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler typically reports a single program location in its error message. This location is the point where the type inference failed, but not necessarily the actual source of the error. Other potential error sources are not even considered. Hence, the compiler often misses the true error source, which increases debugging time for the programmer. In this paper, we present a general framework for automatic localization of type errors. Our algorithm finds all minimum error sources, where the exact definition of minimum is given in terms of a compiler-specific ranking criterion. Compilers can use minimum error sources to produce more meaningful error reports, and for automatic error correction. Our approach works by reducing type inference to constraint satisfaction. We then formulate the problem of computing minimum error sources in terms of weighted maximum satisfiability modulo theories (MaxSMT). Ranking criteria are incorporated by assigning weights to typing constraints. The reduction to MaxSMT allows us to build on decision procedures to support rich type systems.

ABSTRACT. PRSPDL is a highly undecidable propositional dynamic logic with an operator for parallel composition of programs. This operator has a separation semantic such that a multiplicative conjunction similar to the one found in the logic of Boolean bunched implications is definable. The present work identifies an iteration-free decidable fragment of PRSPDL in which the multiplicative conjunction is still definable. A NEXPTIME complexity upper bound for the fragment is given.

ABSTRACT. We introduce a tense logic, called Kt(H,R), arising from logics for spatial reasoning.  Kt(H,R) is a multi-modal logic with two modalities and their converses defined with respect to a pre-order and a relation stable over this pre-order.  We show Kt(H,R) is decidable, it has the effective finite model property and reasoning in Kt(H,R) is PSPACE-complete.  Two complete Hilbert-style axiomatisations are given. The main focus of the paper is tableau-based reasoning.  Our aim is to gain insight into the numerous possibilities of defining tableau calculi and their properties.  We present several labelled tableau calculi for Kt(H,R) in which the theory rules range from accommodating correspondence properties closely, to accommodating Hilbert axioms closely.  The calculi provide the basis for decision procedures that have been implemented and tested on modal and intuitionistic problems. Though the focus is on Kt(H,R), the techniques and ideas used in this research are of general nature and provide a useful methodology for developing practical decision procedures for modal logics, which we will discuss.

The paper is published in "Advances in Modal Logic", Volume 10, 2014.

ABSTRACT. We give a brief survey of the main results on dual tableau-based decision procedures for fragments of the logic of binary relations and we outline our current work in the design of relational decision procedures for logics for order-of-magnitude reasoning. Then we shortly hint at some further research plans on other relational decision procedures.