@article {150,
	title = {A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting},
	year = {2013},
	month = {02/2013},
	type = {Technical Report},
	abstract = {It is well known that it does not exist a condensed goal-independent bottom-up semantics for the full class of term rewriting systems. This kind of semantics is essential for the development of efficacious semantics- based program manipulation tools (e.g. automatic program analyzers and debuggers).

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 {\textquotedblleft}semantically useless{\textquotedblright} elements that can be retrieved from a smaller set of terms.

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compo- sitionally all possible rewritings. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom- up fixpoint characterization.
We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems.

This semantics constitutes the first step for the development of a condensed goal-independent bottom-up fixpoint semantics fully abstract w.r.t. the big-step behavior of rewriting (an ongoing work).},
	keywords = {property-oriented specifications, semantics-based inference methods, TRS},
	author = {Marco Comini and Luca Torella}
}
@proceedings {149,
	title = {TRSynth: a Tool for Automatic Inference of Term Equivalence in Left-linear Term Rewriting Systems},
	journal = {ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM{\textquoteright}13)},
	year = {2013},
	abstract = {In this paper we propose a parametric technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of most general equations relating terms that rewrite, for all possible instantiations, to the same set of normal forms.

The semantic-based inference method that we propose can cope with non-constructor-based TRSs, and considers non-ground terms. Particular emphasis is posed to avoid the generation of {\textquotedblleft}redundant{\textquotedblright} equations that can be a logical consequence of other ones.

To experiment on the validity of our proposal we have considered an instance of the method employing a novel (condensed) semantics for left-linear TRSs and we have implemented a {\textquotedblleft}proof of concept{\textquotedblright} prototype in Haskell which is available online.},
	author = {Marco Comini and Luca Torella}
}
@article {CominiTV11absdiag,
	title = {Abstract Diagnosis for Timed Concurrent Constraint programs},
	journal = {Theory and Practice of Logic Programming},
	volume = {11},
	number = {4-5},
	year = {2011},
	month = {2011},
	pages = {487--502},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency.

In this paper, we provide a general framework for the debugging of tccp programs. To this end, we first present a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems. We also provide an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation.

Given a tccp program and a behavior specification, our debugging approach automatically detects whether the program satisfies the specification. This differs from other semi-automatic approaches to debugging and avoids the need to provide symptoms in advance. We show the efficacy of our approach by introducing an application example. We choose a specific abstract domain and show how we can detect that a program is erroneous.},
	url = {http://users.dimi.uniud.it/~marco.comini/Papers/AbsDiagTCCP/AbsDiagTCCP11.pdf},
	author = {Marco Comini and Laura Titolo and Alicia Villanueva}
}
@article {CominiTV11sem,
	title = {A Compact Goal-Independent Bottom-Up Fixpoint Modeling the Behavior of tccp},
	number = {DIMI-UD/01/2011/RR},
	year = {2011},
	publisher = {Dipartimento di Matematica e Informatica, U. di Udine},
	abstract = {The Timed Concurrent Constraint Language (tccp in short) is a concurrent logic language based on the simple but powerful concurrent constraint paradigm of Saraswat. In this paradigm, the notion of store-as-value is replaced by the notion of store-as-constraint, which introduces some dierences w.r.t. other approaches to concurrency.
In this work, we present a new compact, bottom-up semantics for the language that is well suited for abstract interpretation based debugging and verication purposes in the context of reactive systems. The defined semantics is shown to be correct w.r.t. the behavior of tccp. 
We also propose a an abstract semantics that allows us to effectively implement debugging algorithms based on abstract interpretation. This semantics keeps the particular strong synchronization characteristic of the language.},
	url = {http://users.dimi.uniud.it/~marco.comini/Papers/BotUpBehaTCCP/BotUpBehaTCCP11.pdf},
	author = {Marco Comini and Laura Titolo and Alicia Villanueva}
}
@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.}
}
