Proving Safety Properties of Rewrite Theories

Abstract

Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.

Las teorías de reescritura son un formalismo general y expresivo para especificar sistemas concurrentes en los que los estados se axiomatizan mediante ecuaciones y las transiciones entre estados se axiomatizan mediante reglas de reescritura. Presentamos un enfoque deductivo para verificar las propiedades de seguridad de las teorías de reescritura en el que todo el razonamiento temporal formal sobre las transiciones concurrentes se reduce en última instancia a un razonamiento inductivo puramente ecuacional. Los axiomas de módulo de estrechamiento se utilizan ampliamente en nuestro sistema de inferencia para simplificar aún más las obligaciones de prueba ecuacional a las que se reducen en última instancia todas las fórmulas de prueba de seguridad. De esta manera, las técnicas y herramientas de razonamiento ecuacional existentes se pueden aplicar directamente para verificar las propiedades de seguridad de los sistemas concurrentes. Informamos sobre la implementación de este sistema deductivo en la herramienta Maude Invariant Analyzer, que proporciona un grado sustancial de automatización y puede cumplir automáticamente muchas obligaciones de prueba sin la intervención del usuario.