Sánchez, César

Foto de perfil

E-mails conocidos

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo



Nombre de pila



Nombres alternativos

Sanchez, Cesar

Afiliaciones conocidas

IMDEA Software Institute, Spain
Página completa del ítem
Notificar un error en este autor

Resultados de la búsqueda

Mostrando 1 - 3 de 3
  • Artículo
    Nostralangus: Prophecy-based programming
    Ceresa, Martin; Sánchez, César. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    In this work in progress, we explore the possibility of having a new operator capable of bringing information about the system in the future. While previous works define \emph{prophecy variables} as a way of inspecting the state of the system in the future, we propose to write programs that can actively use such information to choose what agents can do now. Verification techniques define systems where no \textbf{paradoxes} can be introduced but information from the future is still accessible to us as verifiers. In this document, we liberate the programs of such restriction equipping programs with a prophetic conditional operation: \(\ \, \mathcal{P}(\Phi) \, \ \, \mathcal{A} \, \ \, \mathcal{B}\). Actions \(\mathcal{A}\) and \(\mathcal{B}\) are executed depending on a future predicate \(\Phi\) about the system. Both sets of actions \(\mathcal{A}\) and \(\mathcal{B}\) can contradict the prophecy creating paradoxes. We explore how we can rule out some paradoxes appealing to different execution systems and two interpretations of prophecies. One of \emph{possible worlds} where making a prediction generates two possible worlds, one on which the prediction is true and another on which is false. Another interpretation in which the time is linearized using a try-catch interpretation.
  • Artículo
    A SAT-based Efficient Method for the Synthesis from numerical LTL spefications
    Rodriguez, Andoni; Sánchez, César. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.
    Reactive synthesis is the problem of automatically finding a system that satisfies a temporal logic specification, where the atomic propositions are split into those controlled by the system and those controlled by the environment. In this paper we address the problem of the reactive synthesis of specifications that use numerical variables. We consider an approach that transforms the arithmetic specification into a purely Boolean specification by substituting the arithmetic literals by Boolean variables, and computing an additional Boolean requirement that captures the dependencies between the new variables. The resulting specification can be passed to off-the-self Boolean synthesis tools, and is realizable if and only if the original arithmetic specification is. In this paper, we present a method to compute this equi-realizable Boolean specification based on a nested encoding of the search for such a specification using a SAT-solver (for efficiently encoding the search) and an SMT-solver (for checking the decision power of each player) iteratively.
  • Artículo
    On-the-fly reactive synthesis modulo theories
    Rodriguez, Andoni; Sánchez, César. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    The Boolean abstraction technique translates (i.e., Booleanizes) an LTL modulo theories specification into an equi-realizable LTL specification. This solves the realizability modulo theories problem. However, synthesis modulo theories is a different problem: the system has to receive valuations in a first-order theory T and output valuations in T . In this work in progress, we address how to meet this need without a pure synthesis method, but solving ”synthesis” on-the-fly by synthetising a Boolean controller from the Booleanized LTL specification and shipping it with a method that provides models in satisfiable instances of existential formulae (e.g., an SMT solver).