6 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…
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…
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…