Program analysis

URI permanente para esta colección:

https://hdl.handle.net/11705/PROLE/2019/PA
Artículos en la categoría Program analysis publicados en las Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019).
Notificar un error en esta colección

Examinar

Envíos recientes

Mostrando 1 - 2 de 2
  • Miniatura
    Resumen
    Using Well-Founded Relations for Proving Operational Termination
    Lucas, Salvador. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.
    In this paper, we study *operational termination*, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.
  • Miniatura
    Resumen
    Proving Program Properties as First-Order Satisfiability
    Lucas, Salvador. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.
    Program semantics can often be expressed as a (many-sorted) first-order theory $S$, and program properties as sentences $varphi$ which are intended to hold in the *canonical model* of such a theory, which is often incomputable. Recently, we have shown that properties $varphi$ expressed as the existential closure of a boolean combination of atoms can be *disproved* by just finding a model of $S$ and the *negation* $negvarphi$ of $varphi$. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theories. In this paper we extend our previous results to emph{arbitrary} properties, expressed as sentences without any special restriction. Consequently, one can prove a program property $varphi$ by just *finding a model* of an appropriate theory (including $S$ and possibly something else) and an appropriate first-order formula related to $varphi$. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.