@mastersthesis {Bacci11,
	title = {An Abstract Interpretation Framework for Semantics and Diagnosis of Lazy Functional-Logic Languages},
	number = {??},
	year = {2012},
	school = {Universit{\`a} di Udine},
	type = {Ph.D.},
	abstract = {This thesis presents a fixed-point semantics for Curry programs which is fully-abstract with respect to the computed (I/O) behavior. Curry is a declarative language that combines in a seamless way features from functional programming (nested expressions, lazy evaluation, higher-order functions) and logic programming (logical variables, partial data structures, built-in search). Among other proposals, the presented semantics has the following pragmatical features: it is goal-independent, condensed and it is a congruence w.r.t. usage (i.e. unions among modules). We also described an abstract interpretation framework for systematically obtain, from this semantics, several abstract semantics which approximate the (I/O) behavior of a Curry program. These kinds of abstract semantics are particularly suitable for developing efficacious semantics-based program manipulation tools. 
To support this claim some applications as been provided: a static analyzer for groundness dependencies, an abstract debugging/diagnosis method, and an automatic method for synthesizing algebraic property-oriented specifications. Moreover, by means of a program transformation into a Curry semantic-equivalent version, these tools also apply to first order purely functional Haskell programs.},
	keywords = {Abstract Interpretation, Curry, Functional-logic Programming},
	author = {Giovanni Bacci}
}
@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 {BacciC10absdiag,
	title = {Abstract Diagnosis of First Order Functional Logic Programs},
	journal = {Logic-based Program Synthesis and Transformation, 20th International Symposium},
	volume = {6564},
	year = {2011},
	pages = {215--233},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {We present a generic scheme for the abstract debugging of functional logic programs. We associate to programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). 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 provide error symptoms in advance and is applicable with partial specifications and even partial programs.},
	author = {Giovanni Bacci and Marco Comini},
	editor = {Maria Alpuente}
}
@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}
}
@proceedings {ABER11,
	title = {Backward Trace Slicing for Rewriting Logic Theories},
	journal = {23rd International Conference on Automated Deduction, CADE 23},
	year = {2011},
	publisher = {Springer},
	abstract = {Trace slicing is a widely used technique for execution trace 
analysis that is effectively used in program debugging, analysis and comprehension. 
In this paper, we present a 
backward trace slicing technique that can be used  for the analysis of Rewriting Logic theories.

Our trace slicing technique allows us to systematically 
trace back rewrite sequences modulo equational axioms (such as associativity and commutativity)
by means of an  algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data  that do not influence the final result.  
Our methodology is particularly  suitable for analyzing complex, textually-large system computations 
such as those delivered  as counter-example traces by 
Maude model-checkers.},
	keywords = {Maude, Rewriting Logic, Trace Slicing},
	author = {Maria Alpuente and Demis Ballis and J. Espert and Daniel Omar Romero}
}
@article {BK11,
	title = {Special Issue of the Journal of Symbolic Computation on Automated Specification and Verification of Web Systems (Preface)},
	journal = {Journal of Symbolic Computation},
	volume = {46},
	number = {2},
	year = {2011},
	pages = {93{\textendash}94},
	author = {Demis Ballis and Kutsia, T.}
}
@proceedings {BacciC10absdiag,
	title = {Abstract Diagnosis of First Order Functional Logic Programs},
	journal = {Logic-Based Program Synthesis and Transformation {\textendash} 20th International Symposium {\textendash} Pre-Proceedings},
	volume = {10-14},
	year = {2010},
	pages = {58{\textendash}72},
	edition = {20},
	address = {Hagenberg, Austria},
	abstract = {We present a generic scheme for the abstract debugging of functional-logic programs. We associate to our programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the typical cogent features of modern functional-logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). 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.},
	keywords = {Abstract Diagnosis, Debugging, Declarative Diagnosis, Functional-logic Programming},
	author = {Giovanni Bacci and Marco Comini},
	editor = {Maria Alpuente}
}
@article {BacciC10conc,
	title = {A Compact Goal-Independent Bottom-Up Fixpoint Modeling of the Behaviour of First Order Curry},
	number = {6/2010},
	year = {2010},
	publisher = {Dipartimento di Matematica e Informatica, Universit{\`a} di Udine},
	abstract = {This work is motivated by the fact that a {\textquotedblleft}compact{\textquotedblright} semantics for functional logic languages, which is essential for the development of efficacious semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The operational or the rewriting logic semantics that are most commonly considered in func- tional logic are unnecessarily oversized, as they contains many {\textquotedblleft}semantically useless{\textquotedblright} elements that can be retrieved from a smaller set of {\textquotedblleft}basic{\textquotedblright} elements. Therefore, in this article, we present a compressed, goal-independent bottom-up fixpoint semantics that is correct and minimal w.r.t. answers computed for Curry expressions.
We believe that the compactness of the semantics makes it particularly 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.},
	keywords = {Abstract Interpretation, call-time choice semantics, Functional-logic Programming},
	url = {http://www.dimi.uniud.it/comini/Papers/},
	author = {Giovanni Bacci and Marco Comini}
}
@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 {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}
}
@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}
}
@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 {Baggi09,
	title = {An Ontology-based System for Semantic Filtering of XML Data},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {235},
	year = {2009},
	pages = {19{\textendash}33},
	publisher = {Elsevier Science Publishers B. V.},
	address = {Amsterdam, The Netherlands, The Netherlands},
	abstract = {In this paper, we describe a system, written in Haskell, for the ontology-based approximate filtering of XML data. Basically, it allows one to extract relevant data as well as to exclude useless and misleading contents from an XML document. The system provides a declarative language one can use to define XML patterns and ontology queries to express syntactic as well as semantic filtering criteria. The system can be used through a Web application which is endowed with a user-friendly graphical interface. Finally, we provide some meaningful examples which show the usefulness of the implemented filtering methodology.},
	keywords = {Haskell, Ontology-based Approximate Filter, XML},
	issn = {1571-0661},
	doi = {http://dx.doi.org/10.1016/j.entcs.2009.03.003},
	author = {Michele Baggi}
}
@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 {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 {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 {BB08,
	title = {A Lazy Implementation of a Language for Approximate Filtering of XML Documents},
	journal = {Proceedings of the 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007)},
	volume = {216},
	year = {2008},
	pages = {93{\textendash}109},
	publisher = {Elsevier},
	abstract = {In this  paper, we introduce a system, written in Haskell, for filtering information from  XML data.
Essentially, the system implements a simple declarative language which allows one to extract relevant data
as well as to exclude useless and misleading contents from an XML document by matching patterns against XML
documents.

The matching mechanism employes a cost-based pattern transformation algorithm which
searches for patterns in an approximate way (i.e. modulo renaming, insertion, and deletion of XML items)
and ranks the results w.r.t. their cost.
In order to  improve efficiency, the implementation uses sophisticated indexing techniques
and exploits laziness to automatically avoid the construction of unnecessary data structures.

We analyzed both the expressiveness of our filtering language and the performance of the system
using the well known XMark benchmark suite.},
	keywords = {Approximate Filtering of XML, PHIL},
	author = {Michele Baggi and Demis Ballis}
}
@proceedings {BaruzzoC07c,
	title = {A Methodology for UML Models V\&V},
	journal = {Proceedings of First International Conference on Software Testing, Verification, and Validation},
	year = {2008},
	pages = {513{\textendash}516},
	publisher = {IEEE Computer Society},
	abstract = {The introduction of UML models in the software life cycle poses new issues and challenges that are not adequately supported by current state-of-the-art development tools, es- pecially concerning V\&V activities. Indeed, every tool usually focuses on a small set of specialized activities, failing to provide a satisfactory (general purpose) V\&V framework.
In this paper we propose a methodology which allows a seamless integration of V\&V into a UML-based development environment. The methodology exploits a set of sup- porting tools designed to be integrated in a unified frame- work. We believe that such proactive collaboration between tools can reduce significantly both effort and time required to tackle consistency, correctness, quality and long-term maintainability of UML models, increasing the development productivity and the overall quality of the delivered system.},
	isbn = {978-0-7695-3127-4},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BallisBC07b,
	title = {A Minimalist Visual Notation for Design Patterns and Antipatterns},
	journal = {5th International Conference on Information Technology: New Generations},
	year = {2008},
	pages = {51{\textendash}56},
	publisher = {IEEE Computer Society},
	abstract = {Achieving a quality software system requires UML designers to have a good understanding of both design patterns and antipatterns. Unfortunately, UML models for real systems tend to be huge and hard to manage, especially for models automatically generated from source code. Thus, it would be advisable to have tools to automatically identify particular instances of patterns. So, a formal language to express them is needed. However, a textual formalization of such a language is barely usable by UML practitioners. In this paper we propose a visual notation obtained by adding to UML as few graphical elements as possible in order to express both patterns and antipatterns (with the needed formality). This approach has low cognitive load so is easily usable by practitioners but is still rigorous enough for implementation. This notation will be exploited by a GUI front-end for a prototypical tool (that we have recently developed) which is able to discover (anti)patterns in models.
In [3], we proposed a rule-based matching algorithm to identify all instances of a pattern in the graph which underlies the designers{\textquoteright} diagrams. A pattern is given in a general textual language that can express at the same time patterns and antipatterns. However, a formal textual specification is hard to use by UML practitioners. This work was just our first step towards a more ambitious goal: providing a pattern-matching tool that works with a graphical language which extends UML adding as few graphical primitives as possible, yet at the same time retaining the needed precision to be effectively implementable. In this paper we propose such a visual notation. As the additional primitives are really few and intuitive, we believe that this approach involves a reduced cognitive load for the UML designer. Moreover, we developed an algorithm to convert the visual representation of a pattern to an equivalent textual description in terms of the language proposed in [3]. This description can eventually be fed to the prototypical tool that we have developed.},
	doi = {10.1109/ITNG.2008.227},
	author = {Demis Ballis and Andrea Baruzzo and Marco Comini}
}
@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}
}
@mastersthesis {Baruzzo08,
	title = {A Unified Framework for Automated UML Model Analysis},
	year = {2008},
	school = {Dipartimento di matematica e Informatica},
	type = {phd},
	author = {Andrea Baruzzo}
}
@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.}
}
@unpublished {BaruzzoC07,
	title = {A Framework for Computer Aided Consistency Verification of UML Models},
	year = {2007},
	note = {\bibURL{http://www.dimi.uniud.it/comini/Papers/FramCAConVerUML/FramCAConVerUML.pdf}.},
	abstract = {In a UML model, different aspects of a system are covered by different diagrams and this bears the risk that an overall specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a model.

In this paper we propose a static verification framework which checks the mutual consistency of class, statechart, and sequence diagrams (without relying on existent code).

Our approach aims to keep the advantages of static verification and, at the same time, to avoid the weaknesses of other methods, either static or dynamic, which depend on non-UML formalisms. Indeed it does not require developers further (heavy) cognitive load and, moreover, does not force them to keep this external specifications synchronized with the model.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BallisBC07,
	title = {A rule-based method to match Software Patterns against UML Models},
	journal = {The 8th International Workshop on Rule-Based Programming (RULE {\textquoteright}07)},
	year = {2007},
	pages = {239{\textendash}248},
	publisher = {Elsevier Science Publishers},
	address = {North Holland},
	abstract = {In a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes barely tractable by the designer. When the model grows, it is likely that the architectural integrity will be compromised by extensions and bug-fixing operations. Hence, it is important to provide means to help designers to search in big models for particular instances of some variable schema of UML models (design patterns) they construct. This can help them both to find potential problems in the architecture design and to ensure that intended architectural choices had not been broken by mistake. In this paper we propose a rule-based method to find matches of design patterns into a UML model. The method is general enough to tackle most patterns and antipatterns.},
	keywords = {Pattern Matching, Rule-based domain specific language, UML Design Patterns, UML formal specification},
	author = {Demis Ballis and Andrea Baruzzo and Marco Comini}
}
@unpublished {BaruzzoC07b,
	title = {Toward a Unified Framework for Quality and Consistency Verification of UML Models},
	year = {2007},
	note = {\bibURL{http://www.dimi.uniud.it/comini/Papers/FrameworkQualConsUML/FrameworkQualConsUML.pdf}.},
	abstract = {Model-Driven Development (MDD) is an emergent approach to software engineering which is based on the systematic use of software modeling as a primary form of expression. The central focus in MDD is on models, as opposed to source code in the traditional conception of software development. However the introduction of models in the software life cycle poses new issues and challenges that current state-of-the-art development tools do not support adequately.

In this paper we investigate some of these challenges, taking into account the role played by models. Then we propose a unified framework which integrates different verification methods with the intent to check (UML) models against consistency issues and design defects. Our approach aims to integrate traditional techniques with model-based ones, keeping the advantages of both static and dynamic verification methods in order to increase the proficiency of the MDD activities.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BaruzzoC06,
	title = {Checking UML Model Consistency},
	journal = {Proceedings of CILC 2006 - Convegno Italiano di Logica Computazionale},
	year = {2006},
	pages = {1{\textendash}15},
	abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model.
In this work we propose an approach for a static verification of consis- tency of UML models which relies on OCL constraints. Many approaches for model validation and verification rely on generation of suitable code which dynamically (i.e., at run-time) checks the validity of OCL constraints. This approach has several drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem.
On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to real system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with class diagrams, certifies that the dynamic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test sce- narios and also performs the verification of all system properties at the same time.},
	author = {Andrea Baruzzo and Marco Comini}
}
@proceedings {BG06,
	title = {A Rule-based System for Web Site Verification},
	journal = {Proceedings of the 1st International Workshop on Automated Specification and Verification of Web Sites (WWV 2005)},
	volume = {157},
	number = {2},
	year = {2006},
	pages = {153{\textendash}156},
	publisher = {Elsevier},
	abstract = {In this paper, we describe  a system, written in Haskell, for the automated verification of
Web sites which can be used to specify 
(partial) correctness and completeness properties of a given Web site, and then automatically check whether these properties are actually fulfilled.
It provides a rule-based, formal specification language which allows us to
define syntactic/semantic conditions for the Web site by means of a user-friendly graphical interface as well as a verification facility for  recognizing forbidden/incorrect patterns and incomplete/missing Web pages.},
	keywords = {GVERDI, Verification of Web Applications},
	author = {Demis Ballis and Javier Garcia Viv{\'o}}
}
@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 {BaruzzoC06a,
	title = {Static Verification of UML Model Consistency},
	journal = {MoDeV{$^2$}a: Model Development, Validation and Verification},
	year = {2006},
	month = {October},
	pages = {111{\textendash}126},
	publisher = {University of Queensland},
	abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model.
In a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a UML model. In this work we propose an approach for a static verification of consistency of UML models which relies on OCL constraints.
Many approaches for model validation and verification rely on generation of suitable code which dynamically (i.e., at run-time) checks the validity of OCL constraints. This approach has several drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem.
On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to most system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with Class Diagrams, certifies that the dy- namic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test scenarios and also performs the verification of all system properties at the same time.},
	keywords = {OCL, UML diagrams, UML models, Validation, Verification},
	url = {http://modeva.itee.uq.edu.au},
	author = {Andrea Baruzzo and Marco Comini},
	editor = {Hearnden, D. and S{\"u}{\ss}, J. G. and Benoit Baudry and Rapin, N.}
}
@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}
}
@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 {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 {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 {BagnaraCSZ96,
	title = {The AND-compositionality of CLP Computed Answer Constraints},
	journal = {Proceedings APPIA-GULP-PRODE{\textquoteright}96 Joint Conference on Declarative Programming},
	year = {1996},
	pages = {355{\textendash}366},
	abstract = {We present a semantic characterization of CLP languages for the class of quick-checking systems. We define a semantics of computed answer constraints which is AND-compositional, does not loose the distinction between active and passive constraints in the answers and has both a top-down and a bottom-up characterization. We also show that an incrementality property we impose on the constraint solver is essential in order to define an AND-compositional atom-based semantics.},
	author = {Roberto Bagnara and Marco Comini and Francesca Scozzari and Enea Zaffanella},
	editor = {Navarro, M.}
}
@proceedings {CominiL94,
	title = {An Algebraic Theory of Observables},
	journal = {Proceedings of the 1994 Int{\textquoteright}l Symposium on Logic Programming},
	year = {1994},
	pages = {172{\textendash}186},
	publisher = {The MIT Press},
	abstract = {We give an algebraic formalization of SLD-trees and their abstractions (observables). We can state and prove in the framework several useful theorems (AND-compositionality, correctness and full abstraction of the denotation, equivalent top-down and bottom-up constructions) about semantic properties of various observables. Observables are represented by Galois co-insertions and can be used to model abstract interpretation. The constructions and the theorems are inherited by all the observables which can be formalized in the framework. The power of the framework is shown by reconstructing some known examples (answer constraints, call patterns, correct call patterns and ground dependencies call patterns).},
	author = {Marco Comini and Giorgio Levi},
	editor = {Bruynooghe, M.}
}
