@article {FLV08,
	title = {Formal Verification of Websites},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {200},
	number = {3},
	year = {2008},
	pages = {103{\textendash}118},
	abstract = {In this paper, a model for websites is presented. The model is well-suited for the formal verification of dynamic as well as static properties of the system. A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using a model-checking tool on the system. In this setting, we discuss some interesting properties which often need to be checked when designing websites. We have encoded the model using the specification language Maude which allows us to use the Maude model-checking tool.},
	author = {Flores, S. and Salvador Lucas and Alicia Villanueva}
}
@proceedings {FLV07b,
	title = {Formal Verification of Websites},
	journal = {Proceedings of the 16th International Workshop on Automated Specification and Verification of Web Sites (WWV{\textquoteright}07)},
	year = {2007},
	month = {dec},
	pages = {83{\textendash}97},
	address = {San Servolo, Venice, Italy},
	abstract = {In this paper, a model for websites is presented. The model is well-suited for the formal verification of dynamic as well as static properties of the system. A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using a model-checking tool on the system. In this setting, we discuss some interesting properties which often need to be checked when designing websites. We have encoded the model using the specification language Maude which allows us to use the Maude model-checking tool.},
	author = {Flores, S. and Salvador Lucas and Alicia Villanueva},
	editor = {Demis Ballis and Santiago Escobar and Marchiori, M.}
}
@proceedings {FLV07a,
	title = {Using Maude for the Formal Verification of Websites},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	month = {sep},
	pages = {71{\textendash}80},
	address = {Zaragoza (Spain)},
	abstract = {In this paper we address the problem of formal verification of websites by using declarative languages. In particular, we first define a model for websites which can intuitively be specified by using Maude. The model is defined to be well-suited for the formal verification of dynamic as well as static properties of the system.  A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the temporal logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using the Maude model-checking tool. Finally, we have implemented a prototype by using the specification language Maude.},
	author = {Flores, S. and Salvador Lucas and Alicia Villanueva}
}
@proceedings {ABEFL03b,
	title = {Abstract Correction of First-Order Functional Programs},
	journal = {12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003},
	volume = {86},
	number = {3},
	year = {2003},
	publisher = {Elsevier},
	abstract = {Debussy is an (abstract) declarative diagnosis tool for functional
programs  which are written in OBJ style. The debugger  does not require
the user to either provide error symptoms in advance or answer any question
concerning program correctness. 

In this paper, we formalize an inductive learning  methodology
for repairing program bugs in OBJ-like programs.
Correct program rules are automatically synthesized 
from  examples which might be       
generated as an outcome by the Debussy diagnoser.},
	keywords = {Debugging, Inductive Learning, OBJ, program correction},
	author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas}
}
@proceedings {ABEFL03a,
	title = {Abstract Correction of OBJ-like Programs},
	journal = {Informl Proceeding of APPIA GULP PRODE 2003 (AGP 2003)},
	year = {2003},
	pages = {422{\textendash}433},
	author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas}
}
@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.}
}
