@proceedings {ABFOR08,
	title = {An Abstract Generic Framework for Web Site Verification},
	journal = {2008 International Symposium on Applications and the Internet, SAINT 2008},
	year = {2008},
	pages = {104{\textendash}110},
	publisher = {IEEE Computer Society},
	abstract = {In this paper, we present an abstract framework
for Web site verification which improves the performance of a previous, rewriting-based  Web verification methodology.
The approximated framework is formalized as a
source-to-source transformation 
which is parametric w.r.t. the chosen abstraction. This transformation
significantly reduces the size of the Web documents
by dropping or merging
contents that do not
influence the  properties to be checked.
This allows us to reuse all
verification facilities of the previous system WebVerdi-M
to efficiently analyze
Web sites.
In order to ensure that the verified properties are
not affected by the abstraction, 
we develop a methodology which derives
the abstraction of Web sites from their Web specification.
We believe that this methodology can be successfully embedded into
several frameworks. In particular we have developed
a prototypical implementation
which shows a huge speedup w.r.t. a  previous methodology which
did not use this transformation. },
	keywords = {Abstract Verification, Web Site Verification, Web-VERDI},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and P. Ojeda 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}
}
@proceedings {CominiGL00a,
	title = {Logic programs as specifications in the inductive verification of logic programs},
	journal = {Declarative Programming {\textendash} Selected Papers from AGP 2000},
	volume = {48},
	year = {2001},
	note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume48.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume48.html}}}},
	pages = {1{\textendash}16},
	publisher = {Elsevier Science Publishers},
	abstract = {n this paper we define a new verification method based on an assertion language able to express properties defined by the user through a logic program. We first apply the verification framework defined in [CominiGLV99] to derive sufficient inductive conditions to prove partial correctness. Then we show how the resulting conditions can be proved using program transformation techniques.},
	keywords = {Abstract Interpretation, Inductive Verification, Transformation of logic programs},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {Agostino Dovier and Maria Chiara Meo and Omicini, A.}
}
