Ceresa, Martin

Foto de perfil

E-mails conocidos

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo



Nombre de pila



Nombres alternativos

Ceresa, Martín

Afiliaciones conocidas

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

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • 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 Domain-Specific Language for Real-Time Critical Systems
    Parra, Pablo; Ceresa, Martin; Moreno, Elsa; Rodríguez Polo, Óscar; Sánchez, César. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.
    Software development for real-time critical systems is hard, complex and challenging. In real-time critical systems, the imposed requirements are not solely functional, but they also establish a set of temporal constraints that the system must meet to ensure its correct operation. Moreover, validation and verification costs of software development projects for hard real-time critical systems, such as on-board satellite systems, in most cases account for more than half of the total project cost. In this work-in-progress, we introduce a new domain-specific language targetting real-time critical systems aimed at reducing validation and verification costs. The language includes real-time reactive systems abstractions as language citizens, making programs clearer and easier to reason about than current implementations in C or Ada. Moreover, we build the language around two main principles: restricted memory management and every fragment written by users should terminate.