Inductively Verifying Invariants of Rewriting Logic Specifications (2009)
Abstract. We present a novel approach based on inductive theorem proving for verifying invariants of dynamic systems specified in rewriting logic, a formal specification language implemented in the...
Building an Efficient Component for OCL Evaluation ⋆ (2009)
Abstract. In this paper we report on our experience developing the Eye OCL Software (EOS) evaluator, a Java component for efficient OCL evaluation. We first motivate the need for an efficient...
Abstract Automated Analysis of Security-Design Models (2008)
We have previously proposed SecureUML, an expressive UML-based language for constructing security-design models, which are models that combine design specifications for distributed systems with...
Abstract A quick ITP tutorial ∗ (2008)
Manuel Clavel, Miguel Palomino
The ITP tool is an experimental inductive theorem prover for proving properties of Maude equational specifications, i.e., specifications in membership equational logic with an initial algebra...
Abstract. In this paper we present the ITP/OCL tool, a rewritingbased tool that supports automatic validation of UML class diagrams with respect to OCL constraints. Its implementation is directly...
Model Metrication in MOVA: A Metamodel-Based Approach using OCL (2008)
Abstract. We present the metrication facility available in the MOVA tool and discuss its metamodel-based design: metrics in MOVA are OCL queries over the instances (automatically generated by the...
What’s New in Maude 2.4 (2008)
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-oliet, José Meseguer, ...
Abstract. This paper describes the main features introduced in Maude since Maude 2.0, which include: communication with external objects; a new implementation of its module algebra with operations...
MOVA: A Tool for Modeling, Measuring and Validating UML Class Diagrams (2008)
The MOVA tool is a rewriting-based UML [8] modeling, measuring, and validation tool developed as part of a broader effort for integrating rigorous modeling and validation into the software...
Abstract. In this paper we present the ITP/OCL tool, a rewritingbased tool that supports automatic validation of UML static class diagrams with respect to OCL invariants. From a conceptual point of...
Manuel Clavel, Miguel Palomino, Juan Santa-cruz
We propose a design for the integration of decision procedures in reflective rewritingbased equational theorem provers. Rewriting-based equational theorem provers use term rewriting as their basic...
Reflection in General Logics, Rewriting Logic, (2007)
This paper is a summary of my PhD dissertation in which: general axiomatic notions of reflective logic and of strategy, based on the theory of general logics, are proposed; a detailed proof that...
Theorem Proving for Maude's Rewriting Logic (2007)
We present an approach based on inductive theorem proving for verifying invariance properties of systems specified in Rewriting Logic, an executable specification language implemented (among others)...
Theorem Proving for Maude's Rewriting Logic (2007)
We present an approach based on inductive theorem proving for verifying invariance properties of systems specified in Rewriting Logic, an executable specification language implemented (among others)...
Introducing the ITP tool: a tutorial (2007)
Manuel Clavel, Miguel Palomino, Adrián Riesco
Abstract: We present a tutorial of the ITP tool, a rewriting-based theorem prover that can be used to prove inductive properties of membership equational specifications. We also introduce membership...
The Maude formal tool environment (2007)
Manuel Clavel, Francisco Durán, Joe Hendrix, Salvador Lucas, José Meseguer, Peter Ölveczky
Abstract. This paper describes the main features of several tools concerned with the analysis of either Maude specifications, or of extensions of such specifications: the ITP, MTT, CRC, ChC, and SCC...
A metamodel-based approach for analyzing security-design models (2007)
David Basin, Manuel Clavel, Jürgen Doser, Marina Egea
Abstract We have previously proposed an expressive UML-based language for constructing and transforming security-design models, which are models that combine design specifications for distributed...
The Maude formal tool environment (2007)
Manuel Clavel, Francisco Durán, Joe Hendrix, Salvador Lucas, José Meseguer, Peter Ölveczky
Abstract. This paper describes the main features of several tools concerned with the analysis of either Maude specifications, or of extensions of such specifications: the ITP, MTT, CRC, ChC, and SCC...
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-oliet, José Meseguer, ...
ii
Introducing the ITP tool: a tutorial (2007)
Manuel Clavel, Miguel Palomino, Adrián Riesco
Abstract: We present a tutorial of the ITP tool, a rewriting-based theorem prover that can be used to prove inductive properties of membership equational specifications. We also introduce membership...
The Maude formal tool environment (2007)
Manuel Clavel, Joe Hendrix, Salvador Lucas, José Meseguer, Peter Ölveczky
Abstract. This paper describes the main features of several tools concerned with the analysis of either Maude specifications, or of extensions of such specifications: the ITP, MTT, CRC, ChC, and SCC...
Equational specification of UML+OCL static class diagrams (2006)
Abstract. In this paper we propose an equational specification of UML+OCL static class diagrams that provides a formal foundation for automatically validating UML object diagrams with respect to OCL...
A sufficient completeness reasoning tool for partial specifications (2005)
Joe Hendrix, Manuel Clavel, José Meseguer
Abstract. We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with...
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-oliet, José Meseguer, ...
ii
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-oliet, José Meseguer, ...
ii
Reflective Metalogical Frameworks ∗ David Basin Department of Computer Science, ETH Zurich (2003)
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-oliet, José Meseguer, ...
Abstract. This paper gives an overviewof the Maude 2.0 system. We emphasize the full generality with which rewriting logic and membership equational logic are supported, operational semantics issues,...
We show that the generalized variant of rewriting logic where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations,...
Manuel Clavel, José Meseguer, Miguel Palomino
Abstract. We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have...
Manuel Clavel, José Meseguer, Miguel Palomino
Abstract. We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have...
Building equational proving tools by reflection in rewriting logic (2000)
This paper explains the design and use of two equational proving tools, namely an inductive theorem prover---to prove theorems about equational specifications with an initial algebra semantics---and...
Rewriting Logic as a Metalogical Framework (2000)
David Basin, Manuel Clavel, José Meseguer
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
Rewriting Logic as a Metalogical Framework (2000)
David Basin, Manuel Clavel, José Meseguer
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
Maude: Specification and Programming in Rewriting Logic (1999)
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, ...
this paper and his kind help and advice with its L
Internal Strategies in a Reflective Logic (1997)
. After introducing the basic notions of reflective logic and internal strategies, we discuss in detail how reflection can be systematically exploited to design a strategy language internal to a...
Reflection in Rewriting Logic and its Applications in the Maude Language (1997)
this paper applications of reflection in rewriting logic and Maude to the following areas:
Current Design and Implementation of the Cafe Prover and Knuth-Bendix Checker Tools (1997)
Manuel Clavel, Steven Eker, José Meseguer
Introduction The present document gives detailed explanations of our reflective design for the inductive theorem prover and the Knuth-Bendix checker that we are building as part of the Cafe project....
Reflection and Strategies in Rewriting Logic (1996)
After giving general metalogical axioms characterizing reflection in general logics in terms of the notion of a universal theory , this paper specifies a finitely presented universal theory for...
Reflection and Strategies in Rewriting Logic (1996)
After giving general metalogical axioms characterizing reflection in general logics in terms of the notion of a universal theory , this paper specifies a finitely presented universal theory for...
Rewriting logic as a metalogical framework (1974)
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...