@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}
}
@article {ABF06,
	title = {Rule-based Verification of Web Sites},
	journal = {International Journal on Software Tools for Technology Transfer (STTT)},
	volume = {8},
	number = {6},
	year = {2006},
	pages = {565{\textendash}585},
	abstract = {In this paper, we develop a framework for the automated
verification of Web sites which can be used to specify integrity
conditions for a given Web site, and then automatically check
whether these conditions are fulfilled. First, we provide a
rewriting-based, formal specification language which allows us to
define syntactic as well as semantic properties of the Web site.
Then, we formalize a verification technique which detects both
incorrect/forbidden patterns as well as lack of information, that
is, incomplete/missing Web pages, inside the Web site. Useful
information is gathered during the verification process which can
be used  to repair the Web site. Our methodology is based on a
novel  rewriting-based technique, called {\em partial rewriting},
in which the traditional pattern matching mechanism is replaced by
tree  simulation, a suitable technique for recognizing
patterns inside semistructured documents. The framework has been
implemented in the prototype GVerdi, which is publicly
available.},
	keywords = {GVERDI, Homeomorphic Tree embedding, Tree Simulation, Verification of Web Applications},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
