Analysis of Rewriting-Based Systems as First-Order Theories





Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)


CC BY 4.0


Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational properties of such systems can be formulated as first-order sentences F that hold in such a canonical model of S. In this setting, standard results regarding the preservation of satisfiability of different classes of first-order sentences yield a number of interesting applications in program analysis. In particular, properties expressed as existentially quantified boolean combinations of atoms (for instance, a set of unification problems) can then be disproved by just finding an arbitrary model of the considered theory plus the negation of such a sentence. We show that rewriting-based systems fit into this approach. Many computational properties (e.g., infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness, or the secure access to protected pages of a web site) can be investigated in this way. Interestingly, this semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.


Acerca de Lucas, Salvador

Palabras clave

Logical Models, Program Analysis, Rewriting-based Systems
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX