11 citations · 33 across the 25 of their papers we have counts for
21 papers · 1 filter
Towards Relating Ciao Assertions and LPTP Theorems
Marco Pérez, Pedro López-García, Jose F. Morales +2
Abstract interpretation-based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution…
Big-step and small-step Horn clause derivations applied to operational semantics
John P. Gallagher, Manuel Hermenegildo, José Morales +2
The concepts of big-step and small-step derivations are familiar from the operational semantics of programming languages. These concepts are applicable in the more general setting…
Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
Daniela Ferreiro, Daniel Jurjo-Rivas, Marco Ciccalè +3
In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending…
Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
Marco Ciccalè, Daniel Jurjo-Rivas, Jose F. Morales +2
Higher-order constructs enable more expressive and concise code by allowing procedures to be parameterized by other procedures. Assertions allow expressing partial program specific…
Abstract Environment Trimming
Daniel Jurjo-Rivas, Jose F. Morales, Pedro López-García +1
Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many…
An Order Theory Framework of Recurrence Equations for Static Cost Analysis Dynamic Inference of Non-Linear Inequality Invariants
Louis Rustenholz, Pedro Lopez-Garcia, José F. Morales +1
Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without a…
Demonstrating (Hybrid) Active Logic Documents and the Ciao Prolog Playground, and an Application to Verification Tutorials
Daniela Ferreiro, José F. Morales, Salvador Abreu +1
Active Logic Documents (ALD) are web pages which incorporate embedded Prolog engines that run locally within the browser. ALD offers both a very easy way to add click-to-run capabi…
Fifty Years of Prolog and Beyond
Philipp Körner, Michael Leuschel, João Barbosa +8
Both logic programming in general, and Prolog in particular, have a long and fascinating history, intermingled with that of many disciplines they inherited from or catalyzed. A lar…
VeriFly: On-the-fly Assertion Checking via Incrementality
Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Victor Perez-Carrasco +3
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this…
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
John P. Gallagher, Manuel Hermenegildo, Bishoksan Kafle +3
We investigate representations of imperative programs as constrained Horn clauses. Starting from operational semantics transition rules, we proceed by writing interpreters as const…
Towards a General Framework for Static Cost Analysis of Parallel Logic Programs
Maximiliano Klemen, Pedro Lopez-Garcia, John P. Gallagher +2
The estimation and control of resource usage is now an important challenge in an increasing number of computing systems. In particular, requirements on timing and energy arise in a…
Computing Abstract Distances in Logic Programs
Ignacio Casso, Jose F. Morales, Pedro Lopez-Garcia +1
Abstract interpretation is a well-established technique for performing static analyses of logic programs. However, choosing the abstract domain, widening, fixpoint, etc. that provi…
Multivariant Assertion-based Guidance in Abstract Interpretation
Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always…
An Approach to Static Performance Guarantees for Programs with Run-time Checks
Maximiliano Klemen, Nataliia Stulova, Pedro Lopez-Garcia +2
Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program beha…
Incremental and Modular Context-sensitive Analysis
Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo
Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which…
Exploiting Term Hiding to Reduce Run-time Checking Overhead
Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo
One of the most attractive features of untyped languages is the flexibility in term creation and manipulation. However, with such power comes the responsibility of ensuring the cor…
An Approach to Assertion-based Debugging of Higher-Order (C)LP Programs
Nataliia Stulova, José F. Morales, Manuel V. Hermenegildo
Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been i…
Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013)
Rémy Haemmerlé, Jose Morales
This volume contains the papers presented at the 23rd Workshop on Logic-based Methods in Programming Environments (WLPE 2013), which was held in Istanbul, Turkey, on August 24 & 25…
The Ciao clp(FD) Library. A Modular CLP Extension for Prolog
Emilio Jesús Gallego Arias, Rémy Haemmerlé, Manuel V. Hermenegildo +1
We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on C…
Reversible Language Extensions and their Application in Debugging
Zoé Drey, José F. Morales, Manuel V. Hermenegildo
A range of methodologies and techniques are available to guide the design and implementation of language extensions and domain-specific languages. A simple yet powerful technique i…
An overview of Ciao and its design philosophy
M. V. Hermenegildo, F. Bueno, M. Carro +4
We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An import…