Related papers: Calculational Design of [In]Correctness Transforma…
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the…
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness…
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed, using an abstract…
We propose a set of transformation rules for constraint logic programs with negation. We assume that every program is locally stratified and, thus, it has a unique perfect model. We give sufficient conditions which ensure that the proposed…
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and…
Computational psychology has the aim to explain human cognition by computational models of cognitive processes. The cognitive architecture ACT-R is popular to develop such models. Although ACT-R has a well-defined psychological theory and…
The generation of comprehensible explanations is an essential feature of modern artificial intelligence systems. In this work, we consider probabilistic logic programming, an extension of logic programming which can be useful to model…
We present a novel approach to construction of a formal semantics for a programming language. Our approach, using a parametric denotational semantics, allows the semantics to be easily extended to support new language features, and…
Making a Prolog program more efficient by transforming its source code, without changing its operational semantics, is not an obvious task. It requires the user to have a clear understanding of how the Prolog compiler works, and in…
We present necessary and sufficient conditions for the termination of linear homogeneous programs. We also develop a complete method to check termination for this class of programs. Our complete characterization of termination for such…
We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with…
Much work has been done on extending the well-founded semantics to general disjunctive logic programs and various approaches have been proposed. However, these semantics are different from each other and no consensus is reached about which…
In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic…
We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real numbers as limits of Cauchy sequences. We address the…
We present a new approach to termination analysis of logic programs. The essence of the approach is that we make use of general term-orderings (instead of level mappings), like it is done in transformational approaches to logic program…
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system for automatic termination analysis, is…
In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications, in a similar spirit than a set of proof trees. The main…
Tabled logic programming is receiving increasing attention in the Logic Programming community. It avoids many of the shortcomings of SLD execution and provides a more flexible and often extremely efficient execution mechanism for logic…
This paper analyses the declarative readings of logic programming. Logic programming - and negation as failure - has no unique declarative reading. One common view is that logic programming is a logic for default reasoning, a sub-formalism…
We face the problems of correctness, optimality and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two…