Show simple item record

dc.contributor.authorRocha, Camilo
dc.contributor.authorMeseguer, José
dc.description.abstractRewrite 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.eng
dc.description.abstractLas 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.
dc.format.extent15 pá
dc.relation.ispartofseriesLecture Notes in Computer Science;6859
dc.rights© Springer-Verlag Berlin Heidelberg 2011eng
dc.titleProving Safety Properties of Rewrite Theorieseng
dc.typeCapítulo - Parte de Librospa
dc.relation.ispartofbookAlgebra and Coalgebra in Computer Scienceeng
dc.relation.referencesBruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)spa
dc.relation.referencesChandy, K.M., Misra, J.: Parallel Program Design, A foundation. Addison Wesley, Reading (1988)spa
dc.relation.referencesClarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)spa
dc.relation.referencesClavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Bevilacqua, V., Talcott, C.: All About Maude - A High-Performance Logical Framework, 1st edn. LNCS, vol. 4350. Springer, Heidelberg (2007)spa
dc.relation.referencesDurán, F., Meseguer, J.: A church-rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)spa
dc.relation.referencesEscobar, S., Bevilacqua, V.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)spa
dc.relation.referencesFarzan, A., Meseguer, J.: State space reduction of rewrite theories using invisible transitions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 142–157. Springer, Heidelberg (2006)spa
dc.relation.referencesHendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis. University of Illinois at Urbana-Champaign (April 2008)spa
dc.relation.referencesJouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361–373. Springer, Heidelberg (1983)spa
dc.relation.referencesManna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)spa
dc.relation.referencesManna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995)spa
dc.relation.referencesMeseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)spa
dc.relation.referencesMeseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)spa
dc.relation.referencesMeseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theoretical Computer Science 403(2-3), 239–264 (2008)spa
dc.relation.referencesOgata, K., Futatsugi, K.: Proof scores in the oTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)spa
dc.relation.referencesRocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Technical report. University of Illinois at Urbana-Champaign (2010),
dc.relation.referencesRusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 135–150. Springer, Heidelberg (2010)spa
dc.relation.referencesRusu, V., Clavel, M.: Vérification d’invariants pour des systèmes spécifiés en logique de réécriture. Vingtièmes Journées Francophones des Langages Applicatifs 7.2, 317–350 (2009)spa
dc.relation.referencesTiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)spa
dc.relation.referencesViry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)spa
dc.rights.creativecommonsAtribución 4.0 Internacional (CC BY 4.0)spa
dc.subject.armarcComprobación del modelo
dc.subject.armarcRegla de inferencia
dc.subject.armarcTeoría Ecuacional
dc.subject.armarcPropiedad de seguridad
dc.subject.armarcObligación de prueba
dc.subject.proposalModel Checkeng
dc.subject.proposalInference Ruleeng
dc.subject.proposalEquational Theoryeng
dc.subject.proposalSafety Propertyeng
dc.subject.proposalProof Obligationeng

Files in this item


This item appears in the following Collection(s)

Show simple item record

© Springer-Verlag Berlin Heidelberg 2011
Except where otherwise noted, this item's license is described as © Springer-Verlag Berlin Heidelberg 2011