@proceedings {ABER11,
	title = {Backward Trace Slicing for Rewriting Logic Theories},
	journal = {23rd International Conference on Automated Deduction, CADE 23},
	year = {2011},
	publisher = {Springer},
	abstract = {Trace slicing is a widely used technique for execution trace 
analysis that is effectively used in program debugging, analysis and comprehension. 
In this paper, we present a 
backward trace slicing technique that can be used  for the analysis of Rewriting Logic theories.

Our trace slicing technique allows us to systematically 
trace back rewrite sequences modulo equational axioms (such as associativity and commutativity)
by means of an  algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data  that do not influence the final result.  
Our methodology is particularly  suitable for analyzing complex, textually-large system computations 
such as those delivered  as counter-example traces by 
Maude model-checkers.},
	keywords = {Maude, Rewriting Logic, Trace Slicing},
	author = {Maria Alpuente and Demis Ballis and J. Espert and Daniel Omar Romero}
}
@proceedings {ABBF11,
	title = {Completeness of Unfolding for Rewriting Logic Theories},
	journal = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010},
	year = {2010},
	pages = {116{\textendash}123},
	publisher = {IEEE Computer Society Press},
	abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.},
	keywords = {Program Transformation, Rewriting Logic, Unfolding},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {ABBF10,
	title = {A Fold/Unfold Transformation Framework for Rewrite Theories Extended to CCT},
	journal = {ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010},
	year = {2010},
	pages = {43{\textendash}52},
	publisher = {Springer},
	abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a  fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with  functions, rules, equations, sorts,  and algebraic laws (such as commutativity and associativity).
We provide correctness results for the transformation system w.r.t. the semantics of ground reducts.
Moreover, we show how our transformation technique can be naturally
applied to implement a Code Carrying Theory (CCT) system.
CCT is an approach for securing delivery of code from a producer to a consumer
where only a certificate (usually in the form of assertions and proofs)
is transmitted from the producer to the consumer who can check its validity and
then extract executable code from it. Within our framework, the certificate
consists of a sequence of transformation steps which can be applied to
a given consumer specification in order to automatically synthesize  safe
code in agreement with the original requirements. 
We also provide an implementation of  the program transformation framework
in the high-performance, rewriting logic language Maude which, by means of
an experimental evaluation of the system,
highlights the potentiality of our approach.},
	keywords = {CCT, Fold/Unfold Transformations, Program Transformation, Rewriting Logic},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@unpublished {ABER10,
	title = {Model-checking Web Applications with Web-TLR},
	journal = {8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010)},
	year = {2010},
	note = {to appear},
	publisher = {Springer},
	abstract = {Web-TLR is a software tool
designed for model-checking Web applications which is based on rewriting
logic. Web applications are expressed as rewrite theories which  
can be formally verified by using the Maude built-in LTLR model-checker. 

Web-TLR is equipped  with a user-friendly,
graphical Web interface that shields the user from unnecessary information.
Whenever a property is refuted,  an interactive slideshow is generated that allows the user to visually reproduce, step by step,
the erroneous navigation trace that underlies the failing model checking computation.
This provides deep insight into the 
system behavior, which helps to debug Web applications.},
	keywords = {Model-checking, Rewriting Logic, Verification of Web Applications, Web-TLR},
	author = {Maria Alpuente and Demis Ballis and J. Espert and Daniel Omar Romero}
}
@proceedings {ABR09,
	title = {Specification and Verification of Web Applications in Rewriting Logic},
	journal = {16th International Symposium on Formal Methods, FM 2009},
	year = {2009},
	pages = {790{\textendash}805},
	publisher = {Springer},
	abstract = {This paper presents a Rewriting Logic framework that formalizes  the 
interactions between  Web servers and Web browsers through a communicating protocol 
abstracting HTTP.

The proposed framework includes a  scripting language that is powerful enough to model the dynamics of complex  Web applications by
encompassing the main features  of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). 
We also provide a detailed characterization of browser actions (e.g. forward/backward navigation, 
page refresh, and new window/tab openings)  via rewrite rules, and show how our models can be naturally model-checked  by using  the  Linear Temporal Logic of Rewriting (LTLR), which is a  Linear Temporal Logic specifically designed for  model-checking  rewrite theories. 
Our  formalization is particularly suitable for verification purposes, since it allows one to perform in-depth analyses of many subtle aspects related to Web interaction.    
Finally, the framework has been completely implemented in Maude, and we report on some successful experiments  that we  conducted by using the Maude LTLR model-checker.},
	keywords = {Model-checking, Rewriting Logic, Specification of Web Applications, Verification of Web Applications},
	author = {Maria Alpuente and Demis Ballis and Daniel Omar Romero}
}
@proceedings {ABFOR07,
	title = {A Fast Algebraic Web Verification Service},
	journal = {Web Reasoning and Rule Systems, 1st International Conference, RR 2007},
	volume = {4524},
	year = {2007},
	publisher = {Springer},
	abstract = {In this paper, we present the rewriting-based, Web verification  service WebVerdi-M, which   is able to recognize forbidden/incorrect patterns and incomplete/missing Web pages.
WebVerdi-M relies on a   powerful Web verification engine that is written in Maude, which automatically derives the error symptoms. Thanks to the AC pattern matching supported by Maude and its metalevel facilities,   WebVerdi-M enjoys much better performance and usability than a previous implementation of  the verification framework. By using the XML benchmarking  
tool xmlgen,  we develop some scalable experiments which demonstrate the usefulness of our approach.},
	keywords = {Maude, Rewriting Logic, Verification of Web Applications, Web-VERDI},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and P. Ojeda and Daniel Omar Romero}
}
