Conditional narrowing modulo membership equational logic theories with SMT solvers

Abstract

Esta tesis es un estudio sobre cómo mejorar la eficiencia del estrechamiento condicional módulo lógicas ecuacionales de pertenencia para problemas simbólicos de alcanzabilidad en lógica de reescritura, usando el lenguaje Maude. Con este fin, se han analizado distintos enfoques en la tesis. Para cada uno de ellos se ha definido un cálculo de alcanzabilidad y se ha demostrado su corrección y completitud débil. También se han desarrollado varios prototipos para algunos de estos cálculos.La lógica de reescritura es una lógica computacional orientada a la especificación de sistemas concurrentes. Esta lógica se ha diseñado con una semántica matemática precisa que permite probar propiedades de los sistemas especificados. La resolución de problemas de alcanzabilidad en lógica de reescritura es del mayor interés, ya que normalmente está asociada a la comprobación de propiedades de seguridad de las especificaciones...This dissertation is an exploration on how to improve the efficiency of conditional narrowing modulo membership equational logic theories for symbolic reacchability problems in rewriting logic, using he Maude language. To this end, different approaches have been studied in the dissertation. For each of these approaches a reachability calculus has been defined, and a proof of the soundness and weak completeness of the calculus has been given. Also, several prototypes have been developed for some of the calculi.Rewriting logic is an over thirty years old computational logic, that focusses on the specification of concurrent systems. This logic has been designed with a precise mathematical semantics that allows to prove properties of the specified systems. Reachability in rewriting logic, which is usually related to checking the safety properties of specifications, is of the utmost interest...