Publication:
Tool Interoperability in the Maude Formal Environment

Thumbnail Image
Files

Files

Tool Interoperability in the Maude Formal Environment.pdf (185.09 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Durán, Francisco
Rocha, Camilo
Álvarez, José María
Abstract (English)
We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the Church-Rosser Checker, the Coherence Checker, and the Maude Inductive Theorem Prover. We explain the high-level design decisions behind MFE, give a summarized account of its main features, and illustrate with an example the interoperation of the tools available in its current release.
Extent
7 páginas.
Rights

© Springer-Verlag Berlin Heidelberg 2011

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

Collections

AD - CTG – Informática
References

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Bevilacqua, V., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)

Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)

Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 173–178. Springer, Heidelberg (2007)

Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006)

Durán, F., Lucas, S., Meseguer, J.: MTT: The Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313–319. Springer, Heidelberg (2008)

Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (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)

Durán, F., Meseguer, J.: A maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)

Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming Journal of Logic and Algebraic Programming (2011) (accepted for publication)

Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gaducci, F., Montanari, U. (eds.) Proceedings of 4th International Workshop on Rewriting Logic and its Applications (WRLA 2002). Electronic Notes in Theoretical Computer Science, vol. 71 (2002)

Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis. University of Illinois at Urbana-Champaign (2008)

Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of rewrite theories. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 594–609. Springer, Heidelberg (2010)

Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. Tech. rep. University of Illinois at Urbana-Champaign (2010), http://hdl.handle.net/2142/17407