Personne

Rodrigo Raya

Publications associées (7)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Succinct ordering and aggregation constraints in algebraic array theories

Viktor Kuncak, Rodrigo Raya

We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring t ...

Elsevier Science Inc2024

Decision Procedures for Power Structures

Rodrigo Raya

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

The Complexity of Satisfiability Checking for Symbolic Finite Automata

Rodrigo Raya

We study the satisfiability problem of symbolic finite automata and decompose it into the satisfiability problem of the theory of the input characters and the monadic second-order theory of the indices of accepted words. We use our decomposition to obtain ...

2023

The Complexity of Checking Non-Emptiness in Symbolic Tree Automata

Rodrigo Raya

We study the satisfiability problem of symbolic tree automata and decompose it into the satisfiability problem of the existential first-order theory of the input characters and the existential monadic second-order theory of the indices of the accepted word ...

2023

Combinatory Array Logic with Sums

Rodrigo Raya

We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combi- natory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragment ...

2023

On algebraic array theories

Viktor Kuncak, Rodrigo Raya

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...

New York2023

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Springer, Cham2022