@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}
}
@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}
}
@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 {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 {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 {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}
}
