ADDCT 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

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 program- ming 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 mini- mum 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 though, 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.

The paper is to appear 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.