Resumen:
Proving Program Properties as First-Order Satisfiability

Fecha

2019-09-02

Editor

Sistedes

Publicado en

Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019)

Licencia Creative Commons

Resumen

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.

Descripción

Acerca de Lucas, Salvador

Palabras clave

First-Order Logic, Logical Models, Program Analysis
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX