ABSTRACT. Automatic program verification is one of the oldest challenges in computer science. Horn clauses have emerged in recent years as a common representation language for the semantics of imperative programming languages and the modelling of sequential, concurrent and reactive systems. What is the basis for this, and what are the prospects for exploiting it for verification tools? We look at how techniques for analysis and transformation of constraint logic programs are used in verification of imperative programs. These include partial evaluation and abstract interpretation of logic programs, and the exploitation of the connection between tree automata and Horn clauses.

ABSTRACT. We present a new algorithm to compute the Syntactic Closure of a set of functional dependencies, using strategic port graph rewriting. We specify a Visual Domain Specific Language to model relational database schemata as port graphs, and provide an extension to port graph rewriting rules. Using these rules we implement strategies to find the syntactic closure of a set of functional dependencies, analyse the closure and find minimal covers, essential for schema normalisation. We prove soundness and completeness of the computed closure. This methodology is implemented in PORGY, a generic modelling tool that provides a graphical interface and primitives to create and analyse port graph rewriting systems. We illustrate it with examples. Other algorithms to find closures exist, but the strategic graph program provides a visual description of the computation coupled with analysis features not available in other approaches.

ABSTRACT. In this work, which is work in progress, we provide the necessary ingredients for an algorithm capable of searching for semantic clones in CLP program code. Two code fragments are considered semantically cloned when they can both be transformed into a single code fragment thus representing the functionality that is shared between the fragments. While the framework of what constitute such semantic clones has been established before, no algorithm exist that effectively performs the search. We discuss how the generalization of CLP goals can be a driving factor both for controlling the search process (i.e. keeping it finite) as for guiding the search (i.e. choosing what transformations to apply at what moment).

ABSTRACT. Inversion is an important and useful program transformation and has been studied in various programming language paradigms. Semi-inversion is more general than swapping the input and output of a program as in full inversion; instead, parts of the input and output can be swapped freely. This paper introduces a polyvariant semi-inversion algorithm for conditional constructor term rewriting systems. These systems can model both logic and functional languages, which has the advantage that semi-inversion, as well as partial and full inversion, can be studied uniformly across different language paradigms. The algorithm makes use of local inversion and a simple, but effective heuristics, and is shown to be correct. An implementation in Prolog is applied to several inversion problems, including the automatic inversion of a simple encrypter and an inverter for a reversible programming language.

ABSTRACT. The paper presents a new formalism (a minimalist type system) for modeling natural language compositionality over the three levels of compositional semantics, syntax and morphology. The formalism reduces compositionality to a single level by using a subclass of compound types (syntactic compounds of multiple types or their terms) and types for morphemes. The paper includes a detailed comparison with earlier similar approaches and an overview of the implementation of the formalism on a structurally diverse fragment of English in the Coq proof assistant.