In this short paper, we consider non-looping non-termination in term rewriting and logic programming. We describe a strict generalisation of the recurrent pair approach that we introduced previously. We also present an experimental evaluation of our contribution that we implemented in our tool NTI.
CurryInfo is a tool to manage information about program entities defined in modules of Curry packages. CurryInfo is designed as a generic and extensible system so that the kind of information ranges from syntactic (e.g., comments, types, source code) to semantic aspects (e.g., determinism, termination, total definition, non-failing). CurryInfo collects such information and provides various methods to access them. For instance, one can show this information in a REPL or IDE to help the programmer to select or use operations in an appropriate manner. Another application is to include this information in other tools to analyze or verify programs. Since CurryInfo manages a cache containing information about all Curry packages, this can speed up such tools on larger applications.
In this paper, we are interested in the combination of abstract interpretation and interactive theorem proving, which stand at the opposite ends of the program verification automation spectrum. Our idea is to take advantage of the respective strengths of these two techniques. As a first case study, we focus on groundness analysis of logic programs. Using the proof assistant LPTP (Logic Program Theorem Prover), we automate the formal certification of groundness invariants generated by abstract interpretation. We present an experimental evaluation of our approach by applying it to a set of logic programs. Our experiments are twofold. On the one hand, to certify groundness invariants we use automated theorem provers drawing on the theoretical framework of LPTP. On the other hand, we generate and certify natural deduction proofs of groundness invariants with the proof checker of LPTP.
Yul is an intermediate representation that lies in between the (high-level) source code and the (low-level) bytecode languages for Ethereum smart contracts. Although it was proposed to favour the development of verification and optimization techniques, there exists no verifier that can be applied on Yul code directly yet. In this paper, we present a transformational approach to verifying Yul code by transforming it into an equivalent set of Constrained Horn Clauses (CHCs), leading, to the best of our knowledge, to the first approach to directly verify Yul code. Our transformational approach applies the first Futamura projection, i.e., specializes a Yul interpreter written in CHC with respect tothe Yul code to be verified. The verification of the transformed CHC code can rely on existing tools for CHC verification, namely we have used Z3 with the SPACER engine on our case studies.
State variables, loops, and other features of imperative programming languages can bring coding simplification for certain programming idioms that are more cumbersome to express recursively. Because of this, some logic programming systems have incorporated various imperative constructs. FSyntax is a syntactic approach to supporting functional notation in Prolog systems which is based on the use of the syntax and term expansion facilities of the language. Hiord is also a syntactic approach to supporting higher-order in Prolog, building on call/n, and adding other features such as anonymous predicates. Both are used extensively, for example, in the Ciao Prolog system. In this paper, we propose a number of imperative-style constructs based on extending FSyntax and Hiord. These extensions are designed to combine nicely with the basic functional notation and the higher-order facilities, as well as with other extensions, such as constraints. In contrast to other proposals, our approach provides a set of primitives and a higherlevel mechanism that, together, allow users to easily extend the language with features such as array notation, state variables, loops, etc. We illustrate the approach by defining a set of such features and using them to translate idiomatically in imperative style a large collection of small but interesting programs from the Euler Project, for which imperative-style implementations are available in multiple languages. We also show that the approach offers competitive performance.
