5 citations · 7 across the 10 of their papers we have counts for
10 papers
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Louis Rustenholz, Alessio Mansutti, Pedro López-García +3
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate r…
An Approach to the Abstract Interpretation of Goal-Directed Answer Set Programming
Daniel Jurjo-Rivas, Joaquín Arias, Gopal Gupta +3
Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling t…
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…
Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
Louis Rustenholz, Manuel V. Hermenegildo, Pedro Lopez-Garcia +3
We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the f…
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…
Checkification: A Practical Approach for Testing Static Analysis Truths
Daniela Ferreiro, Ignacio Casso, Jose F. Morales +2
Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-pron…
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…
A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs
Louis Rustenholz, Maximiliano Klemen, Miguel Ángel Carreira-Perpiñán +1
Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions…