Automatic proof-search heuristics in the Maude invariant analyzer tool

The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This paper presents the automatic proof-search heuristics at the core of the Maude I...

Full description

Autores:
Rocha, Camilo
Tipo de recurso:
Part of book
Fecha de publicación:
2013
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1837
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1837
Palabra clave:
computability
concurrency control
human computer interaction
inference mechanisms
interactive systems
program verification
rewriting systems
theorem proving
Modelos matemáticos
Modelado orientado a objetos
Sistemas interactivos (computadores)
Sistemas de reescritura
Maude Invariant Analyzer
SMT
Safety
Equations
Mathematical model
Cognition
Algebra
Discharges (electric)
Object oriented modeling
Rights
closedAccess
License
© Copyright 2021 IEEE
id ESCUELAIG2_2dabae2946bba0276b6363690d32ffc8
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1837
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Automatic proof-search heuristics in the Maude invariant analyzer tool
title Automatic proof-search heuristics in the Maude invariant analyzer tool
spellingShingle Automatic proof-search heuristics in the Maude invariant analyzer tool
computability
concurrency control
human computer interaction
inference mechanisms
interactive systems
program verification
rewriting systems
theorem proving
Modelos matemáticos
Modelado orientado a objetos
Sistemas interactivos (computadores)
Sistemas de reescritura
Maude Invariant Analyzer
SMT
Safety
Equations
Mathematical model
Cognition
Algebra
Discharges (electric)
Object oriented modeling
title_short Automatic proof-search heuristics in the Maude invariant analyzer tool
title_full Automatic proof-search heuristics in the Maude invariant analyzer tool
title_fullStr Automatic proof-search heuristics in the Maude invariant analyzer tool
title_full_unstemmed Automatic proof-search heuristics in the Maude invariant analyzer tool
title_sort Automatic proof-search heuristics in the Maude invariant analyzer tool
dc.creator.fl_str_mv Rocha, Camilo
dc.contributor.author.none.fl_str_mv Rocha, Camilo
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.none.fl_str_mv computability
concurrency control
human computer interaction
inference mechanisms
interactive systems
program verification
rewriting systems
theorem proving
topic computability
concurrency control
human computer interaction
inference mechanisms
interactive systems
program verification
rewriting systems
theorem proving
Modelos matemáticos
Modelado orientado a objetos
Sistemas interactivos (computadores)
Sistemas de reescritura
Maude Invariant Analyzer
SMT
Safety
Equations
Mathematical model
Cognition
Algebra
Discharges (electric)
Object oriented modeling
dc.subject.armarc.SPA.fl_str_mv Modelos matemáticos
Modelado orientado a objetos
Sistemas interactivos (computadores)
Sistemas de reescritura
dc.subject.armarc.ENG.fl_str_mv Maude Invariant Analyzer
SMT
dc.subject.proposal.eng.fl_str_mv Safety
Equations
Mathematical model
Cognition
Algebra
Discharges (electric)
Object oriented modeling
description The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This paper presents the automatic proof-search heuristics at the core of the Maude Invariant Analyzer Tool, which provide a substantial degree of automation and can automatically discharge many proof obligations without user intervention. These heuristics can take advantage of equationally defined equality predicates and include rewriting, narrowing, and SMT-based proof-search techniques.
publishDate 2013
dc.date.issued.none.fl_str_mv 2013
dc.date.accessioned.none.fl_str_mv 2021-11-18T13:39:30Z
dc.date.available.none.fl_str_mv 2021-11-18T13:39:30Z
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 9781479910564
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1837
identifier_str_mv 9781479910564
url https://repositorio.escuelaing.edu.co/handle/001/1837
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.ispartofseries.none.fl_str_mv 8CCC;
dc.relation.citationendpage.spa.fl_str_mv 16
dc.relation.citationstartpage.spa.fl_str_mv 9
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.references.spa.fl_str_mv R. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3):386-414 2006.
E. M. Clarke O. Grumberg and D. A. Peled. Model Checking. The MIT Press Cambridge Massachusetts 1999.
M. Clavel F. Duran S. Eker P. Lincoln N. Mart?-Oliet J. Meseguer and C. L. Talcott editors. All About Maude-A High-Performance Logical Framework How to Specify Program and Verify Systems in Rewriting Logic volume 4350 of Lecture Notes in Computer Science. Springer 2007.
M. Clavel and M. Egea. ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In M. Johnson and V. Vene editors AMAST volume 4019 of Lecture Notes in Computer Science pages 368-373. Springer 2006.
F. Duran and J. Meseguer. A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In P. C. Ö lveczky editor WRLA volume 6381 of Lecture Notes in Computer Science pages 69-85. Springer 2010.
F. Duran C. Rocha and J. M. A lvarez. Towards a Maude Formal Environment. In Formal Modeling: Actors Open Systems Biological Systems volume 7000 of Lecture Notes in Computer Science pages 329-351 2011.
R. Gutierrez J. Meseguer and C. Rocha. Order-sorted equality enrichments modulo axioms. In F. Duran editor Rewriting Logic and Its Applications volume 7571 of Lecture Notes in Computer Science pages 162-181. Springer Berlin Heidelberg 2012.
J. Hendrix. Decision Procedures for Equationally Based Reasoning. PhD thesis University of Illinois at Urbana-Champaign April 2008.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1):73-155 1992.
J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce editor WADT volume 1376 of Lecture Notes in Computer Science pages 18-61. Springer 1997.
J. Meseguer and J. A. Goguen. Initially induction and computability. Algebraic Methods in Semantics 1986.
C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD thesis University of Illinois at Urbana-Champaign 2012.
C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. In A. Corradini B. Klin and C. C?rstea editors CALCO volume 6859 of Lecture Notes in Computer Science pages 314-328. Springer 2011.
G. Rosu and A. S tefanescu. Matching Logic: A New Program Verification Approach (NIER Track). In ICSE'11: Proceedings of the 30th International Conference on Software Engineering pages 868-871. ACM 2011.
S. Tang H. Mai and S. T. King. Trust and protection in the illinois browser operating system. In R. H. Arpaci-Dusseau and B. Chen editors OSDI pages 17-32. USENIX Association 2010.
P. Viry. Equational rules for rewriting logic. Theoretical Computer Science 285:487-517 2002.
dc.rights.eng.fl_str_mv © Copyright 2021 IEEE
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 © Copyright 2021 IEEE
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 8 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.place.spa.fl_str_mv Switzerland
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1837/8/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/1837/7/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.png
https://repositorio.escuelaing.edu.co/bitstream/001/1837/9/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/1837/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1837/3/IEEE%20XPLORE.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1837/5/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf.txt
bitstream.checksum.fl_str_mv 6277c1babdae2dc2fd36b81ae30085d3
717205eca36b4e119eefa3ad2d07e14d
f5abe0d315662692989e3b000a1f1548
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_ 1814355631955509248
spelling Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Informática2021-11-18T13:39:30Z2021-11-18T13:39:30Z20139781479910564https://repositorio.escuelaing.edu.co/handle/001/1837The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This paper presents the automatic proof-search heuristics at the core of the Maude Invariant Analyzer Tool, which provide a substantial degree of automation and can automatically discharge many proof obligations without user intervention. These heuristics can take advantage of equationally defined equality predicates and include rewriting, narrowing, and SMT-based proof-search techniques.La herramienta Invariant Analyzer es una herramienta interactiva que mecaniza un sistema de inferencia para probar las propiedades de seguridad de sistemas concurrentes, que pueden ser de estado infinito o cuyo conjunto de estados iniciales puede ser infinito. Este documento presenta las heurísticas de búsqueda automática de pruebas en el núcleo de 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. Estas heurísticas pueden aprovechar los predicados de igualdad definidos ecuacionalmente e incluyen técnicas de reescritura, estrechamiento y búsqueda de pruebas basadas en SMT.8 páginas.application/pdfeng8CCC;169N/AR. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3):386-414 2006.E. M. Clarke O. Grumberg and D. A. Peled. Model Checking. The MIT Press Cambridge Massachusetts 1999.M. Clavel F. Duran S. Eker P. Lincoln N. Mart?-Oliet J. Meseguer and C. L. Talcott editors. All About Maude-A High-Performance Logical Framework How to Specify Program and Verify Systems in Rewriting Logic volume 4350 of Lecture Notes in Computer Science. Springer 2007.M. Clavel and M. Egea. ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In M. Johnson and V. Vene editors AMAST volume 4019 of Lecture Notes in Computer Science pages 368-373. Springer 2006.F. Duran and J. Meseguer. A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In P. C. Ö lveczky editor WRLA volume 6381 of Lecture Notes in Computer Science pages 69-85. Springer 2010.F. Duran C. Rocha and J. M. A lvarez. Towards a Maude Formal Environment. In Formal Modeling: Actors Open Systems Biological Systems volume 7000 of Lecture Notes in Computer Science pages 329-351 2011.R. Gutierrez J. Meseguer and C. Rocha. Order-sorted equality enrichments modulo axioms. In F. Duran editor Rewriting Logic and Its Applications volume 7571 of Lecture Notes in Computer Science pages 162-181. Springer Berlin Heidelberg 2012.J. Hendrix. Decision Procedures for Equationally Based Reasoning. PhD thesis University of Illinois at Urbana-Champaign April 2008.J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1):73-155 1992.J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce editor WADT volume 1376 of Lecture Notes in Computer Science pages 18-61. Springer 1997.J. Meseguer and J. A. Goguen. Initially induction and computability. Algebraic Methods in Semantics 1986.C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD thesis University of Illinois at Urbana-Champaign 2012.C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. In A. Corradini B. Klin and C. C?rstea editors CALCO volume 6859 of Lecture Notes in Computer Science pages 314-328. Springer 2011.G. Rosu and A. S tefanescu. Matching Logic: A New Program Verification Approach (NIER Track). In ICSE'11: Proceedings of the 30th International Conference on Software Engineering pages 868-871. ACM 2011.S. Tang H. Mai and S. T. King. Trust and protection in the illinois browser operating system. In R. H. Arpaci-Dusseau and B. Chen editors OSDI pages 17-32. USENIX Association 2010.P. Viry. Equational rules for rewriting logic. Theoretical Computer Science 285:487-517 2002.© Copyright 2021 IEEEhttps://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_14cbAutomatic proof-search heuristics in the Maude invariant analyzer toolCapí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_970fb48d4fbd8a85Switzerlandcomputabilityconcurrency controlhuman computer interactioninference mechanismsinteractive systemsprogram verificationrewriting systemstheorem provingModelos matemáticosModelado orientado a objetosSistemas interactivos (computadores)Sistemas de reescrituraMaude Invariant AnalyzerSMTSafetyEquationsMathematical modelCognitionAlgebraDischarges (electric)Object oriented modelingORIGINALAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdfAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdfCapítulo - Parte de Libroapplication/pdf518532https://repositorio.escuelaing.edu.co/bitstream/001/1837/8/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf6277c1babdae2dc2fd36b81ae30085d3MD58metadata only accessTHUMBNAILAutomatic proof-search heuristics in the Maude invariant analyzer tool.pngAutomatic proof-search heuristics in the Maude invariant analyzer tool.pngimage/png76596https://repositorio.escuelaing.edu.co/bitstream/001/1837/7/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.png717205eca36b4e119eefa3ad2d07e14dMD57open accessAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdf.jpgAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdf.jpgGenerated Thumbnailimage/jpeg10900https://repositorio.escuelaing.edu.co/bitstream/001/1837/9/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf.jpgf5abe0d315662692989e3b000a1f1548MD59metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1837/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTIEEE XPLORE.pdf.txtIEEE XPLORE.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1837/3/IEEE%20XPLORE.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD53open accessAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdf.txtAutomatic proof-search heuristics in the Maude invariant analyzer tool.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1837/5/Automatic%20proof-search%20heuristics%20in%20the%20Maude%20invariant%20analyzer%20tool.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD55metadata only access001/1837oai:repositorio.escuelaing.edu.co:001/18372022-12-13 03:01:49.68metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Publicaciones similares