View: session overviewtalk overview

13:00 | Politeness for The Theory of Algebraic Datatypes ABSTRACT. Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness. |

13:30 | Combined Covers and Beth Definability PRESENTER: Alessandro Gianola ABSTRACT. Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that cover may not exist in the combined theories. |

14:00 | Possible Models Computation and Revision - A Practical Approach ABSTRACT. This paper is concerned with logic-based modeling and automated reasoning for estimating the current state of a system as it evolves over time. The main motivation is situational awareness, which requires to being able to understand and explain a system's current state, at any time, and at a level that matters to the user, even if only partial or incorrect information about the external events leading to that state is available. The paper proposes to represent such states as models of a logical specification of the properties of interest and a given a set of external timestamped events up to ``now''. The underlying modeling language is a grounded in logic programming, and models are computed in a bottom-up way. It adopts notions of stratification, default negation and a possible model semantics for its (disjunctive) program rules. In order to deal with less-than-perfect event data, the modeling language features a novel model revision operator that allows the programmer to formulate conditions under which a model computation with a corrected set of events should be attempted in an otherwise inconsistent state. Model computation and revision has a long history in the area of logic programming. The novelty of our approach lies in the specifics of the stratification employed, in terms of time and in terms of whether a fact is an external event or derived, and in the specifics of the model revision operator. Our approach deliberately compromises on generality for the benefit of low complexity and any-time reasoning capabilities as needed to support situational awareness application well. The paper provides the technical details of the approach. The main theoretical results are soundness and completeness of the proposed model computation algorithm. On the applied side, the paper describes an implementation as a shallow embedding into the Scala programming language by means of the Scala macro mechanism. This is important in practice, as it gives the programmer built-in access to a full-fledged programming language and its associated libraries. The paper sketches the usefulness of this feature and the model revision operator with a small example for supply chain situational awareness. |

14:30 | SGGS Decision Procedures ABSTRACT. SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala. |

15:15 | Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints |

16:30 | Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols ABSTRACT. The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we add the assumption that certain function symbols f are extensional in the sense that f(s1,...,sn) = f(t1,...,t) implies s1 = t1,...,sn = tn. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP. |

17:00 | A Decision Procedure for String to Code Point Conversion PRESENTER: Andrew Reynolds ABSTRACT. In text-encoding standards such as Unicode, text strings are sequences of code points, each of which can be represented as a natural number. We present a decision procedure for a (concatenation-free) theory of strings that includes length and a conversion function from strings to integer code points. Furthermore, we show that many common string operations, such as conversions between lowercase and uppercase, can be naturally encoded using this conversion function. We implement our approach in the SMT solver CVC4, which contains a state-of-the-art string subsolver, and show that the use of a native procedure for code points significantly improves its performance with respect to other state-of-the-art string solvers. |

17:30 | mu-term: Verify Termination Properties Automatically (system description) ABSTRACT. We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. |

17:45 | Automatically Proving and Disproving Feasibility Conditions ABSTRACT. Given a Conditional Term Rewriting System (CTRS) R and terms s and t, the reachability condition s ->* t is called feasible if there is a substitution σ such that σ(s) ->*_R σ(t) holds; otherwise, it is infeasible. Checking infeasibility of (sequences of) reachability conditions is important in the analysis of computational properties of CTRSs like confluence or operational termination. In this paper, we generalize this notion of feasibility to enable the use of other relations (e.g., subterm |>, context-sensitive rewriting \->, etc.) defined by first-order theories, so that more general properties can be investigated. We introduce a framework for proving feasibility/infeasibility, and a new tool, infChecker, which implements it. |

18:15 | N-PAT: A Nested Model-Checker (system description) ABSTRACT. N-PAT is a new model-checking tool that supports the verification of nested-models -- i.e. models whose behavior depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study. |