Publication:
Automatic proof-search heuristics in the Maude invariant analyzer tool

Thumbnail Image
Files

Files

Automatic proof-search heuristics in the Maude invariant analyzer tool.pdf (506.38 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Abstract (Spanish)
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.
Abstract (English)
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.
Extent
8 páginas.
Rights

© Copyright 2021 IEEE

URI: https://repositorio.escuelaing.edu.co/handle/001/1837
Collections

Collections

AD - CTG – Informática
References

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.