@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 {AlpuenteCEFL02,
	title = {Abstract Diagnosis of Functional Programs},
	journal = {Logic Based Program Synthesis and Tranformation {\textendash} 12th International Workshop, LOPSTR 2002, Revised Selected Papers},
	volume = {2664},
	year = {2003},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {We present a generic scheme for the declarative debugging of functional programs modeled as (conditional) term rewriting systems. We associate to our programs a semantics based on a (continuous) immediate consequence operator, TR, which models the (values/normal forms) semantics of R. Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness.

We have made available a prototypical implementation in Haskell and have tested it on some non trivial examples.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Abstract Verification, Declarative Debugging, Functional Programming, Inductive Verification},
	author = {Maria Alpuente and Marco Comini and Santiago Escobar and Moreno Falaschi and Salvador Lucas},
	editor = {Leuschel, M.}
}
@proceedings {Comini02,
	title = {VeriPolyTypes: a tool for Verification of Logic Programs with respect to Type Specifications},
	journal = {Proceedings of 11th International Workshop on Functional and (constraint) Logic Programming},
	number = {UDMI/18/2002/RR},
	year = {2002},
	pages = {233{\textendash}236},
	publisher = {Dipartimento di Matematica e Informatica, Universit{\`a} di Udine},
	address = {Udine, Italy},
	abstract = {In this system demonstration we present a tool for the verification of Logic Programs w.r.t. type information specifications. The tool is based on sufficient verification conditions obtained by abstract interpretation.

Following the theoretical foundation in [CominiGL01,CominiGLV99entcs,CominiGLV99], the tool is obtained by transforming a static analyzer on a type domain for Logic Programs designed by Codish and Lagoon [CodishL98].},
	keywords = {Abstract Interpretation, Abstract Verification, Inductive Verification, Logic Programming},
	author = {Marco Comini},
	editor = {Moreno Falaschi}
}
