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