3 citations · 4 across the 6 of their papers we have counts for
6 papers
Proving Program Properties as First-Order Satisfiability
Salvador Lucas
Program semantics can often be expressed as a (many-sorted) first-order theory S, and program properties as sentences which are intended to hold in the canonical model of such…
A Semantic Approach to the Analysis of Rewriting-Based Systems
Salvador Lucas
Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in res…
Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving
Salvador Lucas
Recent developments in termination analysis for declarative programs emphasize the use of appropriate models for the logical theory representing the program at stake as a generic a…
Termination of canonical context-sensitive rewriting and productivity of rewrite systems
Salvador Lucas
Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for t…
From matrix interpretations over the rationals to matrix interpretations over the naturals
Salvador Lucas
Matrix interpretations generalize linear polynomial interpretations and have been proved useful in the implementation of tools for automatically proving termination of Term Rewriti…
Removing Redundant Arguments Automatically
Maria Alpuente, Santiago Escobar, Salvador Lucas
The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers u…