ABSTRACT. Proximity relations are binary fuzzy relations, which satisfy reflexivity and symmetry properties, but are not transitive. This relation induces the notion of distance between function symbols, which is further extended to terms. For two given terms we aim at bringing them "sufficiently close" to each other, by finding an appropriate substitution. A similar problem has been addressed earlier with some restrictions, but we consider unrestricted proximal candidates. We present an algorithm which works in two phases: first reducing the unification problem to constraints over sets of function symbols, and then solving the obtained constraints. The problem is decidable and finitary.

ABSTRACT. The nominal approach allows us to extend first-order syntax and represent smoothly systems with variable bindings using, instead of variables, nominal atoms and dealing with renaming through atoms permutations. Nominal unification is, therefore, the extension of first-order unification modulo $\alpha$-equivalence by taking into account this nominal setting. In this work, we present a specification of a nominal C-unification algorithm (nominal unification with commutative operators) in PVS and discuss aspects about the proofs of soundness and completeness. Additionally, the algorithm has been implemented in Python. In relation to the only known specification of nominal C-unification, there are two novel features in this work: first, the formalization of a functional algorithm that can be directly executed (not just a set of non-deterministic inference rules); second, simpler proofs of termination, soundness and completeness, due to the reduction in the number of parameters of the lexicographic measure, from four parameters to only two.

ABSTRACT. Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be elegantly modeled in s(CASP) and how its expressiveness makes it possible to perform deductive and abductive reasoning tasks in domains featuring, for example, constraints involving dense time and fluents.

ABSTRACT. In the blockchain-based, distributed computing platform Ethereum, programs called smart contracts are compiled to bytecode and executed on the Ethereum Virtual Machine (EVM). Executing EVM bytecode is subject to monetary fees---a clear optimization target. Our aim is to superoptimize EVM bytecode by encoding the operational semantics of EVM instructions as SMT formulas and leveraging a constraint solver to automatically find cheaper bytecode. We implement this approach in our EVM Bytecode SuperOptimizer ebso and perform two large scale evaluations on real-world data sets.

ABSTRACT. Landauer's seminal work states that a computation principle can be made reversible by adding the history of the computation, a so-called Landauer embedding, to each state. Although it may seem impractical at first, there are several useful reversibilization techniques that are roughly based on this idea. In this talk, we first introduce a Landauer embedding for a simple (first-order) eager functional language and illustrate its usefulness to define an automatic bidirectionalization technique in the context of bidirectional programming. Then, we extend the language with some primitives for message-passing concurrency and present an appropriate Landauer embedding to make its computations reversible. In this case, we consider reversible debugging as a promising application of reversible computing. Here, the user can explore a computation back and forth in a causal-consistent way (i.e., so that an action is not undone until all the actions that depend on it have already been undone) until the source of a misbehavior is found.

ABSTRACT. We present an approach for assertion-based random testing of Prolog programs and its integration with an assertion-based development model. Our starting point is the Ciao assertion model, a framework that unifies unit testing and run-time verification, as well as static verification and static debugging, using a common assertion language. Properties which cannot be verified statically are checked dynamically. In this context, the idea of generating random test values from assertion preconditions emerges naturally since these preconditions are conjunctions of literals, and the corresponding predicates can in principle be used as generators. Our tool generates valid inputs from the properties that appear in the assertions shared with other parts of the model, and the run time-check instrumentation of the Ciao framework is used to perform a wide variety of checks. This integration also facilitates the combination with static analysis. The generation process is based on running standard predicates under non-standard (random) search rules. Generation can be fully automatic but can also be guided or defined specifically by the user. We propose methods for supporting (C)LP-specific properties, including combinations of shape-based (regular) types and variable sharing and instantiation, and we also provide some ideas for shrinking for these properties. We also provide a case study applying the tools to the verification and checking of the implementations of some of Ciao's abstract domains.

ABSTRACT. Nowadays, many critical systems can be characterized as hybrid ones, combining continuous and discrete behaviours that are closely related. Changes in the continuous dynamics are usually fired by internal or external discrete events. Due to their inherent complexity, it is a crucial but not trivial task to ensure that these systems satisfy some desirable properties. An approach to analyze them consists of the com- bination of model-based testing and run-time verification techniques. In this paper, we present an interval logic to specify properties of event-driven hybrid systems and an automatic transformation procedure of the logic formulae into networks of finite-state machines. Currently, we use Spin and the network of finite-state machines to verify properties on the execution traces provided by event-driven hybrid systems. In particular, we use the approach to analyze mobile applications. The execution traces have been obtained from the TRIANGLE testbed, which implements a controllable network environment for testing, and provides measurements and logs of the mobiles and the network.

ABSTRACT. Logic programming is a declarative programming paradigm. Programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it is incompatible with declarative programming. This report discusses this issue and tries to find how the debugger may be used from the declarative point of view. Also, the box model of Byrd, used by the debugger, is explained in terms of SLD-resolution.

ABSTRACT. Benefits of static type systems are well-known: typically, they offer guarantees that no type error will occur during runtime and, inherently, inferred types serve as documentation on how functions are called. On the other hand, many type systems have to limit expressiveness of the language because, in general, it is undecidable whether a given program is correct regarding types. Another concern that was not addressed so far is that, for logic programming languages such as Prolog, it is impossible to distinguish between intended and unintended failure and, worse, intended and unintended success without additional annotations.

In this paper, we elaborate on and discuss the aforementioned issues. As an alternative, we present a static type analysis which is based on plspec, an optional type system that inserts type checks at runtime. Instead of ensuring full type-safety, we aim to statically identify type errors on a best-effort basis without limiting the expressiveness of Prolog programs. Finally, we evaluate our approach on real-world code featured in the SWI community packages and a large project implementing a model checker.