Arrow Research search

Author name cluster

Albert Rubio

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers
2 author rows

Possible papers

11

SAT Conference 2016 Conference Paper

Speeding up the Constraint-Based Method in Difference Logic

  • Lorenzo Candeago
  • Daniel Larraz
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Albert Rubio

Abstract Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of the program under study as well as the properties to be generated belong to difference logic, i. e. , the fragment of linear arithmetic where atoms are inequalities of the form \(u - v \le k\). However, so far constraint-based techniques have not exploited this fact: in general, Farkas’ Lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system.

Details

SAT Conference 2014 Conference Paper

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions

  • Daniel Larraz
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Albert Rubio

Abstract In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i. e. , enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical. Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraint-based program analysis and show the potential of the method. Finally, we describe how one of these minimal-model-guided techniques can be smoothly adapted to deal with the extension Max-SMT of SMT(NIA) and then applied to program termination proving.

Details

CSL Conference 2008 Invited Paper

The Computability Path Ordering: The End of a Quest

  • Frédéric Blanqui
  • Jean-Pierre Jouannaud
  • Albert Rubio

Abstract In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.

Details

LPAR Conference 2007 Conference Paper

HORPO with Computability Closure: A Reconstruction

  • Frédéric Blanqui
  • Jean-Pierre Jouannaud
  • Albert Rubio

Abstract This paper provides a new, decidable definition of the higher-order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability closure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.

Details

LPAR Conference 2006 Conference Paper

Higher-Order Termination: From Kruskal to Computability

  • Frédéric Blanqui
  • Jean-Pierre Jouannaud
  • Albert Rubio

Abstract Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been an important issue for showing programs correct. In the early days of logic, strong normalization was usually shown by assigning ordinals to expressions in such a way that eliminating a cut would yield an expression with a smaller ordinal. In the early days of verification, computer scientists used similar ideas, interpreting the arguments of a program call by a natural number, such as their size. Showing the size of the arguments to decrease for each recursive call gives a termination proof of the program, which is however rather weak since it can only yield quite small ordinals. In the sixties, Tait invented a new method for showing cut elimination of natural deduction, based on a predicate over the set of terms, such that the membership of an expression to the predicate implied the strong normalization property for that expression. The predicate being defined by induction on types, or even as a fixpoint, this method could yield much larger ordinals. Later generalized by Girard under the name of reducibility or computability candidates, it showed very effective in proving the strong normalization property of typed lambda-calculi with polymorphic types, dependent types, inductive types, and finally a cumulative hierarchy of universes. On the programming side, research on termination shifted from programming to executable specification languages based on rewriting, and concentrated on automatable methods based on the construction on well-founded orderings of the set of terms. The milestone here is Dershowitz’s recursive path ordering (RPO), in the late seventies, whose well-foundedness proof is based on a powerful combinatorial argument, Kruskal’s tree theorem, which also yields rather large ordinals. While the computability predicates must be defined for each particular case, and their properties proved by hand, the recursive path ordering can be effectively automated.

Details

LPAR Conference 2005 Conference Paper

Recursive Path Orderings Can Also Be Incremental

  • Mirtha-Lina Fernández
  • Guillem Godoy
  • Albert Rubio

Abstract In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering \(\sqsupset_{B}\). It can be used for incremental (innermost) termination proofs of hierarchical unions by defining \(\sqsupset_{B}\) as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly.

Details

I&C Journal 2002 Journal Article

A Fully Syntactic AC-RPO

  • Albert Rubio

We present the first fully syntactic (i. e. , non-interpretation-based) AC-compatible recursive path ordering (RPO). It is simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. The ordering is AC-total and defined uniformly for both ground and nonground terms, as well as for partial precedences. More important, it is the first one that can deal incrementally with partial precedences, an aspect that is essential, together with its intuitive behaviour, for interactive applications such as Knuth–Bendix completion.

Details DOI

LPAR Conference 2001 Conference Paper

A Monotonic Higher-Order Semantic Path Ordering

  • Cristina Borralleras
  • Albert Rubio

Abstract There is an increasing use of (first- and higher-order) rewrite rules in many programming languages and logical systems. The recursive path ordering (RPO) is a well-known tool for proving termination of such rewrite rules in the first-order case. However, RPO has some weaknesses. For instance, since it is a simplification ordering, it can only handle simply terminating systems. Several techniques have been developed for overcoming these weaknesses of RPO. A very recent such technique is the monotonic semantic path ordering (MSPO), a simple and easily automatable ordering which generalizes other more ad-hoc methods. Another recent extension of RPO is its higher-order version HORPO. HORPO is an ordering on terms of a typed lambda-calculus generated by a signature of higher-order function symbols. Although many interesting examples can be proved terminating using HORPO, it inherits the weaknesses of the first-order RPO. Therefore, there is an obvious need for higher-order termination orderings without these weaknesses. Here we define the first such ordering, the monotonic higher-order semantic path ordering (MHOSPO), which is still automatable like MSPO. We give evidence of its power by means of several natural and non-trivial examples which cannot be handled by HORPO.

Details

CSL Conference 1996 Conference Paper

Theorem Proving modulo Associativity

  • Albert Rubio

Abstract We present an inference system for first-order constrained clauses with equality modulo associativity (A). Our procedure is refutationally complete and reduces to Knuth-Bendix completion modulo A in the equational case. As an essential ingredient we present the first—as far as we know-A-compatible reduction ordering total on the ground A-congruence classes.

Details

TCS Journal 1995 Journal Article

A total AC-compatible ordering based on RPO

  • Albert Rubio
  • Robert Nieuwenhuis

We define a simplification ordering on terms which is AC-compatible and total on non-AC-equivalent ground terms, without any restrictions on the signature like the number of AC-symbols or free symbols. Unlike previous work by Narendran and Rusinowitch (1991) our AC-RPO ordering is not based on polynomial interpretations, but on a simple extension of the well-known RPO ordering (with a total (arbitrary) precedence on the function symbols). This solves an open question posed e. g. by Bachmair (1992). A second difference is that this ordering is also defined on terms with variables, which makes it applicable in practice for complete theorem proving strategies with built-in AC-unification and for orienting non-ground rewrite systems. The ordering is defined in a simple way by means of rewrite rules, and can be easily implemented, since its main component is RPO.

Details DOI
v2026.09.13