Proving Safety Properties of Rewrite Theories
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 forma...
- Autores:
-
Rocha, Camilo
Meseguer, José
- Tipo de recurso:
- Part of book
- Fecha de publicación:
- 2011
- Institución:
- Escuela Colombiana de Ingeniería Julio Garavito
- Repositorio:
- Repositorio Institucional ECI
- Idioma:
- eng
- OAI Identifier:
- oai:repositorio.escuelaing.edu.co:001/1895
- Acceso en línea:
- https://repositorio.escuelaing.edu.co/handle/001/1895
- Palabra clave:
- Comprobación del modelo
Regla de inferencia
Teoría Ecuacional
Propiedad de seguridad
Obligación de prueba
Model Check
Inference Rule
Equational Theory
Safety Property
Proof Obligation
- Rights
- closedAccess
- License
- © Springer-Verlag Berlin Heidelberg 2011
| id |
ESCUELAIG2_64c0bb7e7e2b6050ff2530c96378b816 |
|---|---|
| oai_identifier_str |
oai:repositorio.escuelaing.edu.co:001/1895 |
| network_acronym_str |
ESCUELAIG2 |
| network_name_str |
Repositorio Institucional ECI |
| repository_id_str |
|
| dc.title.eng.fl_str_mv |
Proving Safety Properties of Rewrite Theories |
| title |
Proving Safety Properties of Rewrite Theories |
| spellingShingle |
Proving Safety Properties of Rewrite Theories Comprobación del modelo Regla de inferencia Teoría Ecuacional Propiedad de seguridad Obligación de prueba Model Check Inference Rule Equational Theory Safety Property Proof Obligation |
| title_short |
Proving Safety Properties of Rewrite Theories |
| title_full |
Proving Safety Properties of Rewrite Theories |
| title_fullStr |
Proving Safety Properties of Rewrite Theories |
| title_full_unstemmed |
Proving Safety Properties of Rewrite Theories |
| title_sort |
Proving Safety Properties of Rewrite Theories |
| dc.creator.fl_str_mv |
Rocha, Camilo Meseguer, José |
| dc.contributor.author.none.fl_str_mv |
Rocha, Camilo Meseguer, José |
| dc.contributor.researchgroup.spa.fl_str_mv |
Informática |
| dc.subject.armarc.none.fl_str_mv |
Comprobación del modelo Regla de inferencia Teoría Ecuacional Propiedad de seguridad Obligación de prueba |
| topic |
Comprobación del modelo Regla de inferencia Teoría Ecuacional Propiedad de seguridad Obligación de prueba Model Check Inference Rule Equational Theory Safety Property Proof Obligation |
| dc.subject.proposal.eng.fl_str_mv |
Model Check Inference Rule Equational Theory Safety Property Proof Obligation |
| description |
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. |
| publishDate |
2011 |
| dc.date.issued.none.fl_str_mv |
2011 |
| dc.date.accessioned.none.fl_str_mv |
2021-12-03T17:10:32Z |
| dc.date.available.none.fl_str_mv |
2021-12-03T17:10:32Z |
| dc.type.spa.fl_str_mv |
Capítulo - Parte de Libro |
| dc.type.coar.fl_str_mv |
http://purl.org/coar/resource_type/c_2df8fbb1 |
| dc.type.coarversion.fl_str_mv |
http://purl.org/coar/version/c_970fb48d4fbd8a85 |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/publishedVersion |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_3248 |
| dc.type.content.spa.fl_str_mv |
Text |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bookPart |
| dc.type.redcol.spa.fl_str_mv |
http://purl.org/redcol/resource_type/ART |
| format |
http://purl.org/coar/resource_type/c_3248 |
| status_str |
publishedVersion |
| dc.identifier.isbn.none.fl_str_mv |
9783642229442 9783642229435 |
| dc.identifier.uri.none.fl_str_mv |
https://repositorio.escuelaing.edu.co/handle/001/1895 |
| identifier_str_mv |
9783642229442 9783642229435 |
| url |
https://repositorio.escuelaing.edu.co/handle/001/1895 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.relation.ispartofseries.none.fl_str_mv |
Lecture Notes in Computer Science;6859 |
| dc.relation.citationendpage.spa.fl_str_mv |
328 |
| dc.relation.citationstartpage.spa.fl_str_mv |
314 |
| dc.relation.indexed.spa.fl_str_mv |
N/A |
| dc.relation.ispartofbook.eng.fl_str_mv |
Algebra and Coalgebra in Computer Science |
| dc.relation.references.spa.fl_str_mv |
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006) Chandy, K.M., Misra, J.: Parallel Program Design, A foundation. Addison Wesley, Reading (1988) Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999) Clavel, 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) Durá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) Escobar, 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) Farzan, 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) Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis. University of Illinois at Urbana-Champaign (April 2008) Jouannaud, 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) Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992) Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995) Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992) Meseguer, 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) Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theoretical Computer Science 403(2-3), 239–264 (2008) Ogata, 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) Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Technical report. University of Illinois at Urbana-Champaign (2010), http://hdl.handle.net/2142/17407 Rusu, 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) Rusu, 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) Tiwari, 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) Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002) |
| dc.rights.eng.fl_str_mv |
© Springer-Verlag Berlin Heidelberg 2011 |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_14cb |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/closedAccess |
| dc.rights.creativecommons.spa.fl_str_mv |
Atribución 4.0 Internacional (CC BY 4.0) |
| rights_invalid_str_mv |
© Springer-Verlag Berlin Heidelberg 2011 https://creativecommons.org/licenses/by/4.0/ Atribución 4.0 Internacional (CC BY 4.0) http://purl.org/coar/access_right/c_14cb |
| eu_rights_str_mv |
closedAccess |
| dc.format.extent.spa.fl_str_mv |
15 páginas. |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Springer |
| dc.publisher.place.spa.fl_str_mv |
Berlín |
| institution |
Escuela Colombiana de Ingeniería Julio Garavito |
| bitstream.url.fl_str_mv |
https://repositorio.escuelaing.edu.co/bitstream/001/1895/6/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.png https://repositorio.escuelaing.edu.co/bitstream/001/1895/7/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdf.jpg https://repositorio.escuelaing.edu.co/bitstream/001/1895/1/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdf https://repositorio.escuelaing.edu.co/bitstream/001/1895/2/license.txt https://repositorio.escuelaing.edu.co/bitstream/001/1895/3/springer.pdf.txt https://repositorio.escuelaing.edu.co/bitstream/001/1895/5/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdf.txt |
| bitstream.checksum.fl_str_mv |
38eaf27d5e5f21011b087aa3cf9c52d8 0dd3bc5e98e3ae5c1d80fa57d6ab0bae be9b098bc4d1ddfff3bec8d431433234 5a7ca94c2e5326ee169f979d71d0f06e d784fa8b6d98d27699781bd9a7cf19f0 d784fa8b6d98d27699781bd9a7cf19f0 |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Escuela Colombiana de Ingeniería Julio Garavito |
| repository.mail.fl_str_mv |
repositorio.eci@escuelaing.edu.co |
| _version_ |
1814355640841142272 |
| spelling |
Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Informática2021-12-03T17:10:32Z2021-12-03T17:10:32Z201197836422294429783642229435https://repositorio.escuelaing.edu.co/handle/001/1895Rewrite 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.15 páginas.application/pdfengSpringerBerlínLecture Notes in Computer Science;6859328314N/AAlgebra and Coalgebra in Computer ScienceBruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)Chandy, K.M., Misra, J.: Parallel Program Design, A foundation. Addison Wesley, Reading (1988)Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Clavel, 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)Durá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)Escobar, 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)Farzan, 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)Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis. University of Illinois at Urbana-Champaign (April 2008)Jouannaud, 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)Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995)Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)Meseguer, 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)Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theoretical Computer Science 403(2-3), 239–264 (2008)Ogata, 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)Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Technical report. University of Illinois at Urbana-Champaign (2010), http://hdl.handle.net/2142/17407Rusu, 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)Rusu, 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)Tiwari, 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)Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)© Springer-Verlag Berlin Heidelberg 2011https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbProving Safety Properties of Rewrite TheoriesCapítulo - Parte de Libroinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85Comprobación del modeloRegla de inferenciaTeoría EcuacionalPropiedad de seguridadObligación de pruebaModel CheckInference RuleEquational TheorySafety PropertyProof ObligationTHUMBNAILProving Safety Properties of Rewrite Theories.pngProving Safety Properties of Rewrite Theories.pngimage/png104113https://repositorio.escuelaing.edu.co/bitstream/001/1895/6/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.png38eaf27d5e5f21011b087aa3cf9c52d8MD56open accessProving Safety Properties of Rewrite Theories.pdf.jpgProving Safety Properties of Rewrite Theories.pdf.jpgGenerated Thumbnailimage/jpeg3473https://repositorio.escuelaing.edu.co/bitstream/001/1895/7/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdf.jpg0dd3bc5e98e3ae5c1d80fa57d6ab0baeMD57open accessORIGINALProving Safety Properties of Rewrite Theories.pdfProving Safety Properties of Rewrite Theories.pdfapplication/pdf189531https://repositorio.escuelaing.edu.co/bitstream/001/1895/1/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdfbe9b098bc4d1ddfff3bec8d431433234MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1895/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTspringer.pdf.txtspringer.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1895/3/springer.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD53open accessProving Safety Properties of Rewrite Theories.pdf.txtProving Safety Properties of Rewrite Theories.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1895/5/Proving%20Safety%20Properties%20of%20Rewrite%20Theories.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD55metadata only access001/1895oai:repositorio.escuelaing.edu.co:001/18952022-12-13 03:01:54.156open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK |