@proceedings {BacciCFV12,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012)},
	volume = {17},
	year = {2012},
	pages = {144-153},
	address = {Budapest, Hungary},
	abstract = {This paper discusses on the additional issues for the automatic inference of algebraic property-oriented specifications which arises because of interaction between laziness and logical variables in lazy functional logic languages.
We present an inference technique that overcomes these issues for the first-order fragment of the lazy functional logic language Curry. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls
that have the same behavior. Our proposal is a (glass-box) semantics-based inference method which can guarantee, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantics-based inference methods},
	isbn = {978-3-939897-43-9},
	issn = {978-3-939897-43-9},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva},
	editor = {Agostino Dovier and V. Santos Costa}
}
@proceedings {BacciCFV12-ICLP,
	title = {The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages},
	journal = {ICLP (Technical Communications)},
	volume = {To appear},
	year = {2012},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik},
	abstract = {This paper discusses on the additional issues for the automatic inference of algebraic property-oriented specifications which arises because of interaction between laziness and logical variables in lazy functional logic languages.
We present an inference technique that overcomes these issues for the first-order fragment of the lazy functional logic language Curry. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. Our proposal is a (glass-box) semantics-based inference method which can guarantee, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@proceedings {BacciCFV12,
	title = {Automatic Synthesis of Specifications for First Order Curry Programs},
	journal = {Proceedings of the 14th symposium on Principles and practice of declarative programming},
	year = {2012},
	pages = {25{\textendash}34},
	publisher = {ACM},
	address = {New York, NY, USA},
	abstract = {This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.},
	keywords = {Curry, property-oriented specifications, semantic-based inference methods},
	isbn = {978-1-4503-1522-7},
	doi = {10.1145/2370776.2370781},
	url = {http://doi.acm.org/10.1145/2370776.2370781},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@proceedings {BacciCFV11,
	title = {Automatic Synthesis of Specifications for Curry Programs},
	journal = {Logic-based Program Synthesis and Transformation, 21th International Symposium {\textendash} Pre-Proceedings},
	year = {2011},
	note = {To appear},
	publisher = {Springer-Verlag},
	address = {Odense, Denmark},
	abstract = {This extended abstract presents a technique to automatically infer specifications from Curry programs. Program specifications (in particular, automatically derived specifications) have been used for program verification, understanding, documentation, service discovering or testing. Our technique, statically infers from the source code of a Curry program a specification which consists of a set of semantic properties that the program operations satisfy. These properties are given by means of equations relating (nested) operation calls that have the same behavior. Our method relies on the semantics of [<a href="http://flit.dimi.uniud.it/?q=biblio/baccic10conc">1</a>] for achieving, to some extent, the correctness of the inferred specification, as opposed to other similar tools based on testing.
In this paper, we present the main ideas of the approach emphasizing the difficulties addressed for the case of the Curry language.},
	keywords = {Abstract Interpretation, Algebraic-oriented Specification, Curry},
	author = {Giovanni Bacci and Marco Comini and Marco Antonio Feli{\'u} and Alicia Villanueva}
}
@article {AlpuenteCEFI08,
	title = {A Compact Fixpoint Semantics for Term Rewriting Systems},
	journal = {Theoretical Computer Science},
	year = {2010},
	note = {To Appear},
	abstract = {This work is motivated by the fact that a {\guillemotleft}compact semantics{\guillemotright} for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many {\guillemotleft}semantically useless{\guillemotright} elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.},
	author = {Maria Alpuente and Marco Comini and Santiago Escobar and Moreno Falaschi and Jos{\`e} Iborra}
}
@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 {AFJV09a,
	title = {Defining Datalog in Rewriting Logic},
	journal = {Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR{\textquoteright}09)},
	volume = {6037},
	year = {2010},
	pages = {188{\textendash}204},
	publisher = {Springer-Verlag},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Schreye, D. de}
}
@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}
}
@article {ABCF10,
	title = {An Integrated Framework for the Diagnosis and Correction of Rule-Based Programs},
	journal = {Theoretical Computer Science},
	volume = {411},
	year = {2010},
	note = {to appear},
	abstract = {We present a generic scheme for the declarative debugging of
programs that are written in rewriting-based languages that are equipped with narrowing.
Our aim is to provide an integrated development
environment in which it is possible to debug a program and
then correct it automatically.

Our methodology is based on the combination (in a single framework) of a semantics-based diagnoser that identifies those parts of the code that contain errors and an inductive learner that tries to repair them, once the bugs have been
located in the program. We develop our methodology in several steps. First, we associate with our programs a semantics
that is based on a (continuous) immediate consequence operator, T_R, which models the answers  computed by
narrowing  and is parametric w.r.t. the evaluation strategy,  which can be eager or lazy. Then, we show that, given the intended specification of a program R, it is possible to check the correctness of R by a single step of T_R.
In order to develop an effective debugging method,
we approximate the computed answers semantics of R
and derive a finitely terminating bottom-up abstract diagnosis method,
which can be used statically.

Finally, a bug-correction  program synthesis methodology attempts to correct the erroneous
components of the wrong code. We propose a hybrid, top-down (unfolding-based)
as well as bottom-up (induction-based), correction approach
that is driven by a set of evidence examples which are
automatically produced as an outcome by the diagnoser.
The resulting program is proven to be correct and complete w.r.t.
the considered example sets.

Our debugging framework does not require the user to  provide
error symptoms in advance or to answer difficult questions concerning
program correctness. An implementation of our debugging
system has been undertaken which
demonstrates the workability of our approach.},
	author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi}
}
@inbook {ABF10,
	title = {Transformation and Debugging of Functional Logic Programs},
	booktitle = {25 Years GULP 2010},
	series = {Lecture Notes in Computer Science},
	year = {2010},
	pages = {271{\textendash}299},
	publisher = {Springer},
	organization = {Springer},
	chapter = {Transformation and Debugging of Functional Logic Programs},
	abstract = {The Italian contribution to 
functional-logic programming has been significant and influential in a number of areas of semantics, and semantics-based program manipulation techniques.
We survey selected topics, with a particular  regard to debugging and 
transformation techniques. These results as usual depend on the
narrowing strategy which is adopted and on the properties satisfied
by the considered programs. In this paper, we restrict ourselves to first-order  functional-logic languages without non-deterministic functions.
We start by describing some basic classical transformation techniques,
namely folding and unfolding.
Then, we recall the
narrowing-driven partial evaluation, which is the first generic algorithm for 
the specialization of functional logic   programs. 
Regarding debugging,
we describe a goal-independent approach to automatic diagnosis and correction 
which applies the immediate consequence operator modeling computed answers
to the diagnosis of bugs in functional logic programs.
A companion bug-correction  program synthesis methodology is 
described that attempts to correct the erroneous
components of the wrong code.},
	keywords = {Debugging, Fold/Unfold Transformations, Functional-logic Programming, Program Transformation},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
@article {AFJV09b,
	title = {DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {248},
	year = {2009},
	pages = {57{\textendash}66},
	abstract = {This work presents a practical Java program analysis framework that is obtained by combining a Java virtual
machine with a general-purpose verification toolbox that we previously extended. In our methodology,
Datalog clauses are used to specify complex interprocedural program analyses involving dynamically created
objects. After extracting an initial set of Datalog constraints about the Java bytecode program semantics,
our framework transforms the Datalog rules of a particular analysis into a Boolean Equation System (Bes),
whose local resolution using the aforementioned extended verification toolbox corresponds to the demand-
driven computation of the analysis.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}
}
@article {AFJV09tr,
	title = {Defining Datalog in Rewriting Logic},
	number = {DSIC-II/07/09},
	year = {2009},
	publisher = {DSIC, Universidad Polit{\'e}cnica de Valencia},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}
}
@proceedings {AFJV09,
	title = {Implementing Datalog in Maude},
	journal = {Proceedings of the IX Jornadas sobre Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}09) and I Taller de Programaci{\'o}n Funcional (TPF{\textquoteright}09)},
	year = {2009},
	month = {September},
	pages = {15{\textendash}22},
	abstract = {Transformation of programs among different paradigms has been widely studied in academic research and education. The interest on Datalog has recently increased as a specification language for expressing, in just a few lines, complex interprocedural analyses involving dynamically created objects. In real-world problems, the Datalog rules encoding a particular analysis must be solved generally under a huge set of Datalog facts that are automatically extracted from the analyzed program (e.g. pointer dependencies). In that context, this work aims at exploiting Maude{\textquoteright}s capabilities for supporting efficient evaluation of Datalog queries. We demonstrate how, starting from an almost straightforward transformation of Datalog programs into Maude specifications, we are able to achieve a highly efficient version.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Pe{\~n}a, R.}
}
@proceedings {BBF09,
	title = {Quantitative Pathway Logic for Computational Biology},
	journal = {Computational Methods in Systems Biology, 7th International Conference, CMSB 2009},
	number = {5688},
	year = {2009},
	pages = {68{\textendash}82},
	publisher = {Springer},
	abstract = {This paper presents an extension of Pathway Logic, called Quantitative Pathway Logic (QPL), which allows one to reason about quantitative aspects of biological processes, such as element concentrations and reactions kinetics. Besides, it supports the modeling of inhibitors, that is, chemicals which may block a given reaction whenever their concentration exceeds a certain threshold. QPL models can be specified and directly simulated using rewriting logic or can be translated into Discrete Functional Petri Nets (DFPN) which are a subclass of Hybrid Functional Petri Nets in which only discrete transitions are allowed. Under some constraints over the anonymous variables appearing in the QPL models, the transformation between the two computational models is shown to preserve computations. By using the DFPN representation our models can be graphically visualized and simulated by means of well known tools (e.g. Cell Illustrator); moreover standard Petri net analyses (e.g. topological analysis,  forward/backward reachability, etc.) may be performed on the net model.
An executable framework for QPL and for the translation of QPL models into DFPNs has been implemented using the rewriting-based language Maude. We have tested this system on several examples},
	keywords = {Bioinformatics, Petri nets, Quantitative Pathway Logic, Rewriting Logic},
	author = {Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {AFJV08,
	title = {Using Datalog and Boolean Equation Systems for Program Analysis},
	journal = {Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS{\textquoteright}08)},
	volume = {5596},
	year = {2009},
	pages = {215{\textendash}231},
	publisher = {Springer-Verlag},
	abstract = {This paper describes a powerful, fully automated method to evaluate Datalog queries by using Boolean Equation Systems (Bess), and its application to object-oriented program analysis. Datalog is used as a specification language for expressing complex interprocedural program analyses involving dynamically created objects. In our methodology, Datalog rules encoding a particular analysis together with a set of constraints (Datalog facts that are automatically extracted from program source code) are dynamically transformed into a Bes, whose local resolution corresponds to the demand-driven evaluation of the program analysis. This approach allows us to reuse existing general purpose verification toolboxes, such as Cadp, providing local Bes resolutions with linear-time complexity. Our evaluation technique has been implemented and successfully tested on several Java programs and Datalog analyses that demonstrate the feasibility of our approach.},
	author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva},
	editor = {Darren Cofer and Alessandro Fantechi}
}
@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}
}
@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 {ABBF08,
	title = {Semantic Verification of Web System Contents},
	journal = {ER 2008 Workshops (WISM 2008)},
	volume = {5232},
	year = {2008},
	pages = {437{\textendash}446},
	publisher = {Springer},
	abstract = {In this paper, we present a rule-based
specification language to define and automatically check semantic as
well as syntactic constraints over the informative content of a Web
system. The language is inspired by the GVERDI language and
significantly extends it by integrating ontology reasoning into the
specification rules and by adding new syntactic constructs.  The
resulting language  increases the expressiveness of the original one
and enables a more sophisticated treatment of the semantic
information related to the contents of the Web system.},
	keywords = {Description logic, OWL, Semantic Verification, Web Site Verification},
	author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@proceedings {BBF08,
	title = {XML Semantic Filtering via Ontology Reasoning},
	journal = {3rd International Conference on Internet and Web Applications and Services, ICIW 2008},
	year = {2008},
	pages = {482{\textendash}487},
	publisher = {IEEE Computer Society},
	abstract = {In this paper, we present an extension of PHIL, a declarative language
for filtering information from XML data. The proposed approach allows us to extract relevant data as well as to exclude useless and
misleading contents from an XML document.
Essentially, it combines ontology reasoning with an approximate pattern-matching engine which searches for patterns in a flexible way (i.e. modulo
renaming, insertion, and deletion of XML items) and ranks the
results w.r.t. their cost. 
The filtering process is guided by the syntax as well as the semantics of the XML documents, since it relies on both the document structure and the ontological information to which the document is related.
Such information is retrieved by querying (possibly remote) ontology reasoners.
Ontology reasoning capabilities are integrated into  the filtering language via an adapted version of the DIG interface, which is a standard framework for describing description logic systems. Our extension to the DIG interface allows one to deal with non-ground ontology queries.  },
	keywords = {Approximate Filtering of XML, Description logic, DIG, OWL, PHIL, Semantic Filtering},
	author = {Michele Baggi and Demis Ballis and Moreno Falaschi}
}
@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 {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}
}
@article {FV06,
	title = {Automatic Verification of Timed Concurrent Constraint programs},
	journal = {Theory and Practice of Logic Programming},
	volume = {6},
	number = {3},
	year = {2006},
	pages = {265{\textendash}300},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Alicia Villanueva}
}
@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}
}
@proceedings {ABFR06,
	title = {A Semi-Automatic Methodology for Repairing Faulty Web Sites},
	journal = {4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006)},
	year = {2006},
	pages = {31{\textendash}40},
	publisher = {IEEE Computer Society},
	abstract = {The development and maintenance of Web sites are difficult tasks. To
maintain the consistency of ever-larger,  complex Web sites, Web administrators
need effective mechanisms that assist them in fixing every possible
inconsistency. In this paper, we present a novel methodology for
semi-automatically repairing faulty Web sites which can be
integrated on top of an existing rewriting-based verification
technique developed in a previous work. Starting from a categorization
of the kinds of errors that can be found during the Web
verification activities, we formulate a stepwise transformation
procedure that achieves correctness and completeness of the Web
site w.r.t. its formal specification while respecting the structure of
the document (e.g. the schema of an XML document).

Finally, we shortly describe  a prototype implementation of the repairing tool
which we used for an experimental evaluation of our method.},
	keywords = {Web site debugging, Web site repair},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and Daniel Omar Romero}
}
@proceedings {ABF05,
	title = {A Rewriting-based Framework for Web Sites Verification},
	journal = {Proceedings of the 5th International Workshop on Rule-Based Programming (RULE 2004)},
	year = {2005},
	pages = {41{\textendash}61},
	publisher = {Elsevier},
	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 obtains
the requirements not fulfilled by the Web site, and helps to repair  the errors by finding out   incomplete information and/or missing pages. 
Our methodology is based on a novel  rewriting-based technique, called  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 Web verification system   Verdi which is publicly available.},
	keywords = {partial rewriting, Tree Simulation, VERDI, verification of Web sites},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
@inbook {AFV04,
	title = {A Symbolic Model checker for tccp Programs},
	booktitle = {Proceedings of the International Workshop on Rapid Integration of Software Ingeneering techniques (RISE{\textquoteright}04)},
	series = {Lecture Notes in Computer Science},
	volume = {3475},
	year = {2005},
	pages = {45{\textendash}56},
	publisher = {Springer Verlag},
	organization = {Springer Verlag},
	keywords = {cc, model checking, symbolic representation},
	author = {Maria Alpuente and Moreno Falaschi and Alicia Villanueva}
}
@proceedings {ABF04b,
	title = {An Automated Tool for Web Sites Verification},
	journal = {Logics in Artificial Intelligence, 9th European Conference, JELIA 2004},
	volume = {3229},
	year = {2004},
	pages = {726{\textendash}729},
	publisher = {Springer},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
@proceedings {ABF04a,
	title = {Automated Verification of Web Sites Using Partial Rewriting},
	journal = {Pre-Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004},
	year = {2004},
	pages = {81{\textendash}88},
	author = {Maria Alpuente and Demis Ballis and Moreno Falaschi}
}
@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.}
}
@proceedings {ABCF03,
	title = {Correction of Functional Logic Programs},
	journal = {Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003},
	volume = {2618},
	year = {2003},
	pages = {54{\textendash}68},
	publisher = {Springer},
	abstract = {We propose a new methodology for synthesizing correct
functional logic programs.  We aim to create an integrated development
environment in which it is possible to debug a program and correct
it automatically. We start from a declarative diagnoser that we have developed
previously which allows us
to identify wrong  program rules w.r.t. an intended specification.
Then a bug-correction, program synthesis methodology tries
to correct the erroneous components of the wrong code.
We propose a hybrid, top-down  (unfolding-based)
as well as bottom-up (induction-based), approach
for the automatic correction of functional logic programs
which is driven by a set of evidence examples which are automatically
produced as an outcome by the diagnoser.
The resulting program is proven to be correct and complete
w.r.t. the considered example sets.
Finally, we also provide a prototypical implementation
which we use for an experimental
evaluation of our system.
},
	keywords = {Debugging, Functional-logic Programming, program correction, Program Transformation, Unfolding},
	author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi}
}
@proceedings {BFFHR03,
	title = {Cost-Sensitive Diagnosis of Declarative Programs},
	journal = {12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003},
	volume = {86},
	year = {2003},
	pages = {3},
	publisher = {Elsevier},
	abstract = {Diagnosis methods in debugging aim at detecting bugs of a program,
 either by comparing it with a correct specification or 
by the help of an oracle (usually the user herself).
 Debugging techniques for declarative programs usually
 exploit the semantical properties of programs (and specifications)
 and generally try to detect one or more buggy rules.
 In this way, rules are split apart in an absolute way:
 either they are correct or not. However, in many situations, 
not every error has the same consequences, an issue that is 
ignored by classical debugging frameworks.
 In this paper, we generalise debugging by considering a cost function,
 i.e. a function that assigns different cost values to each
 kind of error and different benefit values to each kind of correct response. 
The problem is now redefined as assigning a real-valued probability 
and cost to each rule, by considering each rule more or
 less  guilty of the overall error and cost of the program. 
This makes possible to rank rules rather than only separate
 them between right and wrong. 
Our debugging method is also different from classical approaches
 in that it is probabilistic, i.e. we use a set of ground
 examples to approximate these rankings. },
	keywords = {Cost Matrixes, Cost-sensitive Evaluation, Debugging, Functional-logic Programming},
	author = {Demis Ballis and Moreno Falaschi and C. Ferri and J. Hern{\'a}ndez-Orallo and M. Jos{\'e} Ramirez-Quintana}
}
@proceedings {AFV03b,
	title = {Symbolic Model Checking for Timed Concurrent Constraint Programs},
	journal = {Proceedings of the III Jornadas de Programaci{\'o}n y Lenguajes},
	year = {2003},
	address = {Alicante},
	keywords = {cc, model checking, symbolic representation},
	author = {Maria Alpuente and Moreno Falaschi and Alicia Villanueva}
}
@proceedings {ABCF02,
	title = {A Multiparadigm Automatic Correction Scheme},
	journal = {Pre-Proceedings of the 11th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2002},
	year = {2002},
	author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi}
}
@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}
}
@proceedings {FPV01,
	title = {Time Limited Model Checking},
	journal = {Proceedings of International Workshop on Specification Analysis and Validation for Emerging Technologies in Computational Logic (SAVE{\textquoteright}01)},
	year = {2001},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva},
	editor = {Delzanno, G. and Etalle, S. and Gabbrielli, M.}
}
@proceedings {FPV00a,
	title = {Modeling Timed Concurrent systems in a Temporal Concurrent Constraint language},
	journal = {Proceedings of the 2000 Joint Conference on Declarative Programming},
	year = {2000},
	publisher = {University of La Habana},
	address = {La Habana, Cuba},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva}
}
@article {FPV00b,
	title = {Modeling Timed Concurrent systems in a Temporal Concurrent Constraint language - I},
	journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
	volume = {48},
	year = {2000},
	pages = {1{\textendash}15},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva}
}
@proceedings {CominiLV97,
	title = {Modular Abstract Diagnosis},
	journal = {Proceedings APPIA-GULP-PRODE{\textquoteright}98 Joint Conference on Declarative Programming},
	year = {1998},
	pages = {409{\textendash}420},
	abstract = {The paper extends the Abstract Diagnosis framework to Modular Abstract Diagnosis, where we are concerned with programs composed of separate modules. Our theory of abstract diagnosis can be applied to modular diagnosis even if our concrete semantics is not OR-compositional. Abstract diagnosis is a generalization of declarative diagnosis, where we consider operational properties, i.e. observables, which are properties which can be extracted from a goal computation.},
	keywords = {Debugging, Declarative Diagnosis, Logic Programming, Semantics, Verification},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Freire-Nistal, J. L. and Moreno Falaschi and Villares-Ferro, M.}
}
@proceedings {CominiLV94,
	title = {Abstract Debugging of Logic Programs},
	journal = {Proc. Logic Program Synthesis and Transformation and Metaprogramming in Logic 1994},
	volume = {883},
	year = {1994},
	pages = {440{\textendash}450},
	publisher = {Springer-Verlag},
	abstract = {Abstract debugging of logic programs is a novel combination of three known techniques, i.e. algorithmic (declarative) debugging, the s-semantics approach to the definition of program denotations modeling various observable behaviors, and abstract interpretation.},
	author = {Marco Comini and Giorgio Levi and Vitiello, G.},
	editor = {Fribourg, L. and Turini, F.}
}
