Automatic proof-search heuristics in the Maude invariant analyzer tool

Rocha, Camilo

dc.contributor.author	Rocha, Camilo
dc.date.accessioned	2021-11-18T13:39:30Z
dc.date.available	2021-11-18T13:39:30Z
dc.date.issued	2013
dc.identifier.isbn	9781479910564
dc.identifier.uri	https://repositorio.escuelaing.edu.co/handle/001/1837
dc.description.abstract	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.	eng
dc.description.abstract	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.	spa
dc.format.extent	8 páginas.	spa
dc.format.mimetype	application/pdf	spa
dc.language.iso	eng	spa
dc.relation.ispartofseries	8CCC;
dc.rights	© Copyright 2021 IEEE	eng
dc.rights.uri	https://creativecommons.org/licenses/by/4.0/	spa
dc.title	Automatic proof-search heuristics in the Maude invariant analyzer tool	eng
dc.type	Capítulo - Parte de Libro	spa
dc.type.version	info:eu-repo/semantics/publishedVersion	spa
oaire.accessrights	http://purl.org/coar/access_right/c_14cb	spa
oaire.version	http://purl.org/coar/version/c_970fb48d4fbd8a85	spa
dc.contributor.researchgroup	Informática	spa
dc.publisher.place	Switzerland	spa
dc.relation.citationendpage	16	spa
dc.relation.citationstartpage	9	spa
dc.relation.indexed	N/A	spa
dc.relation.references	R. Bruni and J. Meseguer. Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3):386-414 2006.	spa
dc.relation.references	E. M. Clarke O. Grumberg and D. A. Peled. Model Checking. The MIT Press Cambridge Massachusetts 1999.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	J. Hendrix. Decision Procedures for Equationally Based Reasoning. PhD thesis University of Illinois at Urbana-Champaign April 2008.	spa
dc.relation.references	J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1):73-155 1992.	spa
dc.relation.references	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.	spa
dc.relation.references	J. Meseguer and J. A. Goguen. Initially induction and computability. Algebraic Methods in Semantics 1986.	spa
dc.relation.references	C. Rocha. Symbolic Reachability Analysis for Rewrite Theories. PhD thesis University of Illinois at Urbana-Champaign 2012.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	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.	spa
dc.relation.references	P. Viry. Equational rules for rewriting logic. Theoretical Computer Science 285:487-517 2002.	spa
dc.rights.accessrights	info:eu-repo/semantics/closedAccess	spa
dc.rights.creativecommons	Atribución 4.0 Internacional (CC BY 4.0)	spa
dc.subject.armarc	computability
dc.subject.armarc	concurrency control
dc.subject.armarc	human computer interaction
dc.subject.armarc	inference mechanisms
dc.subject.armarc	interactive systems
dc.subject.armarc	program verification
dc.subject.armarc	rewriting systems
dc.subject.armarc	theorem proving
dc.subject.armarc	Modelos matemáticos	SPA
dc.subject.armarc	Modelado orientado a objetos	SPA
dc.subject.armarc	Sistemas interactivos (computadores)	SPA
dc.subject.armarc	Sistemas de reescritura	SPA
dc.subject.armarc	Maude Invariant Analyzer	ENG
dc.subject.armarc	SMT	ENG
dc.subject.proposal	Safety	eng
dc.subject.proposal	Equations	eng
dc.subject.proposal	Mathematical model	eng
dc.subject.proposal	Cognition	eng
dc.subject.proposal	Algebra	eng
dc.subject.proposal	Discharges (electric)	eng
dc.subject.proposal	Object oriented modeling	eng
dc.type.coar	http://purl.org/coar/resource_type/c_3248	spa
dc.type.content	Text	spa
dc.type.driver	info:eu-repo/semantics/bookPart	spa
dc.type.redcol	http://purl.org/redcol/resource_type/ART	spa