papers: publish TRs for icalp 2013 and zephyrus
[homepage.git] / research / publications.mdwn
index 40b3d8d..2480600 100644 (file)
@@ -7,47 +7,58 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed journals">international, peer-reviewed journal articles</span>
 
 
 # <span title="international, peer-reviewed journals">international, peer-reviewed journal articles</span>
 
- 1. <a class="bibtex-download" href="infsof2012-mpm.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **A Modular Package Manager Architecture**.  <em>To appear in <a href="http://www.journals.elsevier.com/information-and-software-technology/">Information
-      and Software Technology</a>, Elsevier.</em>
+ 1. <a class="paper-download" href="infsof2012-mpm.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="infsof2012-mpm.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.infsof.2012.09.002" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **A Modular Package Manager Architecture**.  <em>In <a href="http://www.journals.elsevier.com/information-and-software-technology/">Information
+      and Software Technology</a>,
+      Volume 55, Issue 2,
+      <a href="http://www.sciencedirect.com/science/article/pii/S0950584912001851">pp. 459-474</a>.
+      ISSN 0950-5849, Elsevier,
+      February 2013.</em>
     [[!toggle id=id42 text="Abstract..."]] [[!toggleable id=id42 text="""
     [[!toggle id=id42 text="Abstract..."]] [[!toggleable id=id42 text="""
-    *Abstract:* The success of modern software distributions in the Free and Open Source world can be explained, among other factors, by the availability of a large collection of software packages and the possibility to easily install and remove those components using state of the art package managers. However, package managers are often built using a monolithic architecture and hard-wired and ad-hoc dependency solvers implementing some customized heuristics. In this paper we propose a modular architecture relying on precise interface formalisms that allows the system administrator to choose from a variety of dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, offer more expressive preference languages, and be easily adaptable to new platforms. We have built a working prototype—called MPM—following the design advocated in this paper, and we show how it largely outperforms a variety of state of the art package managers.
-    """]]
- 1. <a class="paper-download" href="jss2012-concern.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jss2012-concern.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.jss.2012.02.018" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Dependency Solving: a Separate Concern in Component Evolution Management**.  <em>To appear in <a href="http://www.journals.elsevier.com/journal-of-systems-and-software/">Journal
-      of Systems and Software</a>, Elsevier.</em>
+    *Abstract:* The success of modern software distributions in the Free and Open Source world can be explained, among other factors, by the availability of a large collection of software packages and the possibility to easily install and remove those components using state of the art package managers. However, package managers are often built using a monolithic architecture and hard-wired and ad-hoc dependency solvers implementing some customized heuristics. In this paper we propose a modular architecture relying on precise interface formalisms that allows the system administrator to choose from a variety of dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, offer more expressive preference languages, and be easily adaptable to new platforms. We have built a working prototype, called MPM, following the design advocated in this paper, and we show how it largely outperforms a variety of state of the art package managers.
+    """]]
+ 1. <a class="paper-download" href="jss2012-concern.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jss2012-concern.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.jss.2012.02.018" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Dependency Solving: a Separate Concern in Component Evolution Management**.  <em>In <a href="http://www.journals.elsevier.com/journal-of-systems-and-software/">Journal
+      of Systems and Software</a>,
+      Volume 85, Issue 10,
+      <a href="http://www.sciencedirect.com/science/article/pii/S0164121212000477">pp. 2228-2240</a>.
+      ISSN 0164-1212, Elsevier,
+      October 2012.</em>
     [[!toggle id=id40 text="Abstract..."]] [[!toggleable id=id40 text="""
     *Abstract:* Maintenance of component-based software platforms often has to face rapid evolution of software components. Component dependencies, conflicts, and package managers with dependency solving capabilities are the key ingredients of prevalent software maintenance technologies that have been proposed to keep software installations synchronized with evolving component repositories. We review state-of-the-art package managers and their ability to keep up with evolution at the current growth rate of popular component-based platforms, and conclude that their dependency solving abilities are not up to the task. We show that the complexity of the underlying upgrade planning problem is NP-complete even for seemingly simple component models, and argue that the principal source of complexity lies in multiple available versions of components. We then discuss the need of expressive languages for user preferences, which makes the problem even more challenging. We propose to establish dependency solving as a separate concern from other upgrade aspects, and present CUDF as a formalism to describe upgrade scenarios. By analyzing the result of an international dependency solving competition, we provide evidence that the proposed approach is viable.
     """]]
  1. <a class="paper-download" href="ahci2012-wiki.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="ahci2012-wiki.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1155/2012/893575" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, Francesco Draicchio, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Constrained Wiki: The WikiWay to Validating Content**.  <em>In <a href="http://www.hindawi.com/journals/ahci/">Advances in Human-Computer
       Interaction</a>, Volume 2012, Article ID
     [[!toggle id=id40 text="Abstract..."]] [[!toggleable id=id40 text="""
     *Abstract:* Maintenance of component-based software platforms often has to face rapid evolution of software components. Component dependencies, conflicts, and package managers with dependency solving capabilities are the key ingredients of prevalent software maintenance technologies that have been proposed to keep software installations synchronized with evolving component repositories. We review state-of-the-art package managers and their ability to keep up with evolution at the current growth rate of popular component-based platforms, and conclude that their dependency solving abilities are not up to the task. We show that the complexity of the underlying upgrade planning problem is NP-complete even for seemingly simple component models, and argue that the principal source of complexity lies in multiple available versions of components. We then discuss the need of expressive languages for user preferences, which makes the problem even more challenging. We propose to establish dependency solving as a separate concern from other upgrade aspects, and present CUDF as a formalism to describe upgrade scenarios. By analyzing the result of an international dependency solving competition, we provide evidence that the proposed approach is viable.
     """]]
  1. <a class="paper-download" href="ahci2012-wiki.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="ahci2012-wiki.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1155/2012/893575" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, Francesco Draicchio, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Constrained Wiki: The WikiWay to Validating Content**.  <em>In <a href="http://www.hindawi.com/journals/ahci/">Advances in Human-Computer
       Interaction</a>, Volume 2012, Article ID
-      893575, <a href="http://www.hindawi.com/journals/ahci/2012/893575/">pp. 1-19</a>. Hindawi,
-      2012</em>
+      893575, <a href="http://www.hindawi.com/journals/ahci/2012/893575/">pp. 1-19</a>.
+      Hindawi, 2012</em>
     [[!toggle id=id39 text="Abstract..."]] [[!toggleable id=id39 text="""
     *Abstract:* The "WikiWay" is the open editing philosophy of wikis meant to foster open collaboration and continuous improvement of their content. Just like other online communities, wikis often introduce and enforce conventions, constraints, and rules for their content, but do so in a considerably softer way, expecting authors to deliver content that satisfies the conventions and the constraints, or, failing that, having volunteers of the community, the WikiGnomes, fix others' content accordingly. Constrained wikis is our generic framework for wikis to implement validators of community-specific constraints and conventions that preserve the WikiWay and their open collaboration features. To this end, specific requirements need to be observed by validators and a specific software architecture can be used for their implementation, that is, as independent functions (implemented as internal modules or external services) used in a nonintrusive way. Two separate proof-of-concept validators have been implemented for MediaWiki and MoinMoin, respectively, providing an annotated view functions, that is, presenting content authors with violation warnings, rather than preventing them from saving a noncompliant text.
     """]]
  1. <a class="paper-download" href="scp2010-evolution.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="scp2010-evolution.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.scico.2010.11.001" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Supporting Software Evolution in Component-Based FOSS Systems**.  <em>In <a href="http://www.elsevier.com/locate/scico/">Science
       of Computer Programming</a>, Volume 76, Issue
     [[!toggle id=id39 text="Abstract..."]] [[!toggleable id=id39 text="""
     *Abstract:* The "WikiWay" is the open editing philosophy of wikis meant to foster open collaboration and continuous improvement of their content. Just like other online communities, wikis often introduce and enforce conventions, constraints, and rules for their content, but do so in a considerably softer way, expecting authors to deliver content that satisfies the conventions and the constraints, or, failing that, having volunteers of the community, the WikiGnomes, fix others' content accordingly. Constrained wikis is our generic framework for wikis to implement validators of community-specific constraints and conventions that preserve the WikiWay and their open collaboration features. To this end, specific requirements need to be observed by validators and a specific software architecture can be used for their implementation, that is, as independent functions (implemented as internal modules or external services) used in a nonintrusive way. Two separate proof-of-concept validators have been implemented for MediaWiki and MoinMoin, respectively, providing an annotated view functions, that is, presenting content authors with violation warnings, rather than preventing them from saving a noncompliant text.
     """]]
  1. <a class="paper-download" href="scp2010-evolution.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="scp2010-evolution.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.scico.2010.11.001" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Supporting Software Evolution in Component-Based FOSS Systems**.  <em>In <a href="http://www.elsevier.com/locate/scico/">Science
       of Computer Programming</a>, Volume 76, Issue
-      12, pp. 1144-1160. ISSN 0167-6423,
+      12,
+      <a href="http://www.sciencedirect.com/science/article/pii/S0167642310002005">pp. 1144-1160</a>.
+      ISSN 0167-6423,
       Elsevier, 2011.</em>
     [[!toggle id=id35 text="Abstract..."]] [[!toggleable id=id35 text="""
       Elsevier, 2011.</em>
     [[!toggle id=id35 text="Abstract..."]] [[!toggleable id=id35 text="""
-    *Abstract:* FOSS (Free and Open Source Software) systems present interesting challenges in system evolution. On one hand, most FOSS systems are based on very fine-grained units of soft- ware deployment—called packages—which promote system evolution; on the other hand, FOSS systems are among the largest software systems known and require sophisticated static and dynamic conditions to be verified, in order to successfully deploy upgrades on user machines. The slightest error in one of these conditions can turn a routine upgrade into a system administrator nightmare. In this paper we introduce a model-based approach to support the upgrade of FOSS systems. The approach promotes the simulation of upgrades to predict failures before affecting the real system. Both fine-grained static aspects (e.g. configuration incoher- ences) and dynamic aspects (e.g. the execution of configuration scripts) are taken into account, improving over the state of the art of upgrade planners. The effectiveness of the approach is validated by instantiating the approach to widely-used FOSS distributions.
+    *Abstract:* FOSS (Free and Open Source Software) systems present interesting challenges in system evolution. On one hand, most FOSS systems are based on very fine-grained units of software deployment, called packages, which promote system evolution; on the other hand, FOSS systems are among the largest software systems known and require sophisticated static and dynamic conditions to be verified, in order to successfully deploy upgrades on user machines. The slightest error in one of these conditions can turn a routine upgrade into a system administrator nightmare. In this paper we introduce a model-based approach to support the upgrade of FOSS systems. The approach promotes the simulation of upgrades to predict failures before affecting the real system. Both fine-grained static aspects (e.g. configuration incoherences) and dynamic aspects (e.g. the execution of configuration scripts) are taken into account, improving over the state of the art of upgrade planners. The effectiveness of the approach is validated by instantiating the approach to widely-used FOSS distributions.
     """]]
  1. <a class="paper-download" href="nrhm-overlapping-conversions.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="nrhm-overlapping-conversions.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1080/13614560802316145" title="Document Object Identifier">doi&gt;</a></span> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Towards the unification of formats for overlapping markup**.  <em>
        In <a href="http://www.tandf.co.uk/journals/titles/13614568.asp">New Review
        of Hypermedia and Multimedia</a>, <a href="http://www.informaworld.com/smpp/title~content=t713599880~db=all~tab=issueslist~branches=14#v14">Volume
        14</a>, <a href="http://www.informaworld.com/smpp/title~content=g903097087~db=all">Issue
        1</a>, January 2008, <a href="http://www.informaworld.com/smpp/content~db=all?content=10.1080/13614560802316145">pp. 57-94</a>.
     """]]
  1. <a class="paper-download" href="nrhm-overlapping-conversions.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="nrhm-overlapping-conversions.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1080/13614560802316145" title="Document Object Identifier">doi&gt;</a></span> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Towards the unification of formats for overlapping markup**.  <em>
        In <a href="http://www.tandf.co.uk/journals/titles/13614568.asp">New Review
        of Hypermedia and Multimedia</a>, <a href="http://www.informaworld.com/smpp/title~content=t713599880~db=all~tab=issueslist~branches=14#v14">Volume
        14</a>, <a href="http://www.informaworld.com/smpp/title~content=g903097087~db=all">Issue
        1</a>, January 2008, <a href="http://www.informaworld.com/smpp/content~db=all?content=10.1080/13614560802316145">pp. 57-94</a>.
-       <a href="http://www.tandf.co.uk/">Taylor and Francis</a>, <a href="http://www.informaworld.com/smpp/title~content=t713599880~link=cover">ISSN
+       <a href="http://www.tandf.co.uk/">Taylor and Francis</a>,
+       <a href="http://www.informaworld.com/smpp/title~content=t713599880~link=cover">ISSN
        1361-4568</a>.
       </em>
     [[!toggle id=id20 text="Abstract..."]] [[!toggleable id=id20 text="""
        1361-4568</a>.
       </em>
     [[!toggle id=id20 text="Abstract..."]] [[!toggleable id=id20 text="""
-    *Abstract:* Overlapping markup refers to the issue of how to represent data structures more expressive than trees—for example direct acyclic graphs—using markup (meta-)languages which have been designed with trees in mind—for example XML. In this paper we observe that the state of the art in overlapping markup is far from being the widespread and consistent stack of standards and technologies readily available for XML and develop a roadmap for closing the gap. In particular we present in the paper the design and implementation of what we believe to be the first needed step, namely: a syntactic conversion framework among the plethora of overlapping markup serialization formats. The algorithms needed to perform the various conversions are presented in pseudo-code, they are meant to be used as blueprints for researchers and practitioners which need to write batch translation programs from one format to the other.
+    *Abstract:* Overlapping markup refers to the issue of how to represent data structures more expressive than trees, for example direct acyclic graphs, using markup (meta-)languages which have been designed with trees in mind, for example XML. In this paper we observe that the state of the art in overlapping markup is far from being the widespread and consistent stack of standards and technologies readily available for XML and develop a roadmap for closing the gap. In particular we present in the paper the design and implementation of what we believe to be the first needed step, namely: a syntactic conversion framework among the plethora of overlapping markup serialization formats. The algorithms needed to perform the various conversions are presented in pseudo-code, they are meant to be used as blueprints for researchers and practitioners which need to write batch translation programs from one format to the other.
     """]]
  1. <a class="paper-download" href="mcs-disambiguation-errors.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mcs-disambiguation-errors.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/s11786-008-0058-2" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Spurious Disambiguation Errors and How to Get Rid of Them**.  <em>
        In <a href="http://www.springerlink.com/content/1661-8270">Mathematics in
        Computer Science</a>, Volume 2, Number
        2, <a href="http://www.springerlink.com/content/1p816h3610g8k854/">pp. 355-378</a>,
     """]]
  1. <a class="paper-download" href="mcs-disambiguation-errors.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mcs-disambiguation-errors.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/s11786-008-0058-2" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Spurious Disambiguation Errors and How to Get Rid of Them**.  <em>
        In <a href="http://www.springerlink.com/content/1661-8270">Mathematics in
        Computer Science</a>, Volume 2, Number
        2, <a href="http://www.springerlink.com/content/1p816h3610g8k854/">pp. 355-378</a>,
-       December 2008. Springer Birkhäuser, <a href="http://www.springerlink.com/content/1661-8270">ISSN
-       1661-8270</a>.
+       December 2008. Springer Birkhäuser,
+       <a href="http://www.springerlink.com/content/1661-8270">ISSN 1661-8270</a>.
       </em>
     [[!toggle id=id19 text="Abstract..."]] [[!toggleable id=id19 text="""
     *Abstract:* The disambiguation approach to the input of formulae enables users of mathematical assistants to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae however, far too many typing errors are generated; among them we want to present only errors related to the formula interpretation meant by the user, hiding errors related to other interpretations. We study disambiguation errors and how to classify them into the spurious and genuine error classes. To this end we give a general presentation of the classes of disambiguation algorithms and efficient disambiguation algorithms. We also quantitatively assess the quality of the presented error classification criteria benchmarking them in the setting of a formal development of constructive algebra.
       </em>
     [[!toggle id=id19 text="Abstract..."]] [[!toggleable id=id19 text="""
     *Abstract:* The disambiguation approach to the input of formulae enables users of mathematical assistants to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae however, far too many typing errors are generated; among them we want to present only errors related to the formula interpretation meant by the user, hiding errors related to other interpretations. We study disambiguation errors and how to classify them into the spurious and genuine error classes. To this end we give a general presentation of the classes of disambiguation algorithms and efficient disambiguation algorithms. We also quantitatively assess the quality of the presented error classification criteria benchmarking them in the setting of a formal development of constructive algebra.
@@ -64,6 +75,12 @@ in reverse chronological order.
     *Abstract:* Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, mostly characterized by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.
     """]]
 
     *Abstract:* Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, mostly characterized by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.
     """]]
 
+# editorials
+
+ 1. <a class="paper-download" href="spe-wt-2012-editorial.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="spe-wt-2012-editorial.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1002/spe.2169" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://www.cs.unibo.it/~rossi/">Davide Rossi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Editorial**.  <em>To appear in <a href="http://onlinelibrary.wiley.com/journal/10.1002/(ISSN)1097-024X">Software:
+      Practice and Experience</a>. ISSN 1097-024X,
+      Wiley, 2013.</em>
+
 # book chapters
 
  1. <a class="paper-download" href="web30-semantics-templating.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="web30-semantics-templating.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Web Semantics via Wiki Templating**.  <em>
 # book chapters
 
  1. <a class="paper-download" href="web30-semantics-templating.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="web30-semantics-templating.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Web Semantics via Wiki Templating**.  <em>
@@ -80,7 +97,23 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed conferences">international, peer-reviewed conference proceedings</span>
 
 
 # <span title="international, peer-reviewed conferences">international, peer-reviewed conference proceedings</span>
 
- 1. <a class="paper-download" href="sefm2012-aeolus.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sefm2012-aeolus.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, <a href="http://www.cs.unibo.it/~zavattar/">Gianluigi Zavattaro</a>. **Towards a Formal Component Model for the Cloud**.  <em>In proceedings of SEFM 2012: <a href="http://sefm2012.city.academic.gr/">10th International Conference on
+ 1. <a class="paper-download" href="fmco2012-foss-components.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="fmco2012-foss-components.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Formal Aspects of Free and Open Source Software Components**.  <em>In proceedings of FMCO 2012: <a href="http://www.cs.unibo.it/hats-fmoc/">HATS International School on
+      Formal Models for Components and Objects</a>, Bertinoro,
+      Italy, 24-28 September 2012. LNCS 7866,
+      pp. 216-239,
+      Springer-Verlag, 2013.</em>
+    [[!toggle id=id49 text="Abstract..."]] [[!toggleable id=id49 text="""
+    *Abstract:* Free and Open Source Software (FOSS) distributions are popular solutions to deploy and maintain software on server, desktop, and mobile computing equipment. The typical deployment method in the FOSS setting relies on software distributions as vendors, packages as independently deployable components, and package managers as upgrade tools. We review research results from the past decade that apply formal methods to the study of inter-component relationships in the FOSS context. We discuss how those results are being used to attack both issues faced by users, such as dealing with upgrade failures on target machines, and issues important to distributions such as quality assurance processes for repositories containing tens of thousands, rapidly evolving software packages.
+    """]]
+ 1. <a class="paper-download" href="icalp2013-aeolus.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="icalp2013-aeolus.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.cs.unibo.it/~jmauro/">Jacopo Mauro</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, <a href="http://www.cs.unibo.it/~zavattar/">Gianluigi Zavattaro</a>. **Component Reconfiguration in the Presence of Conflicts**.  <em>To appear in proceedings of ICALP 2013: <a href="http://www.icalp2013.lu.lv/">40th International Colloquium on
+      Automata, Languages and Programming</a>, Riga, Latvia, 8-12
+      July, 2013.  LNCS 7966,
+      pp. 187-198, Springer-Verlag,
+      2013.</em>
+    [[!toggle id=id45 text="Abstract..."]] [[!toggleable id=id45 text="""
+    *Abstract:* Components are traditionally modeled as black-boxes equipped with interfaces that indicate provided/required ports and, often, also conflicts with other components that cannot coexist with them. In modern tools for automatic system management, components become grey-boxes that show relevant internal states and the possible actions that can be acted on the components to change such state during the deployment and reconfiguration phases. However, state-of-the-art tools in this field do not support a systematic management of conflicts. In this paper we investigate the impact of conflicts by precisely characterizing the increment of complexity on the reconfiguration problem.
+    """]]
+ 1. <a class="paper-download" href="sefm2012-aeolus.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sefm2012-aeolus.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-642-33826-7_11" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, <a href="http://www.cs.unibo.it/~zavattar/">Gianluigi Zavattaro</a>. **Towards a Formal Component Model for the Cloud**.  <em>In proceedings of SEFM 2012: <a href="http://sefm2012.city.academic.gr/">10th International Conference on
       Software Engineering and Formal Methods</a>, Thessaloniki,
       Greece, 1-5 October, 2012. LNCS 7504,
       pp. 156-171, Springer-Verlag,
       Software Engineering and Formal Methods</a>, Thessaloniki,
       Greece, 1-5 October, 2012. LNCS 7504,
       pp. 156-171, Springer-Verlag,
@@ -88,25 +121,29 @@ in reverse chronological order.
     [[!toggle id=id43 text="Abstract..."]] [[!toggleable id=id43 text="""
     *Abstract:* We consider the problem of deploying and (re)configuring resources in a "cloud" setting, where interconnected software components and services can be deployed on clusters of heterogeneous (virtual) machines that can be created and connected on-the-fly. We introduce the Aeolus component model to capture similar scenarii from realistic cloud deployments, and instrument automated planning of day-to-day activities such as software upgrade planning, service deployment, elastic scaling, etc. We formalize the model and characterize the feasibility and complexity of configuration achievability in Aeolus.
     """]]
     [[!toggle id=id43 text="Abstract..."]] [[!toggleable id=id43 text="""
     *Abstract:* We consider the problem of deploying and (re)configuring resources in a "cloud" setting, where interconnected software components and services can be deployed on clusters of heterogeneous (virtual) machines that can be created and connected on-the-fly. We introduce the Aeolus component model to capture similar scenarii from realistic cloud deployments, and instrument automated planning of day-to-day activities such as software upgrade planning, service deployment, elastic scaling, etc. We formalize the model and characterize the feasibility and complexity of configuration achievability in Aeolus.
     """]]
- 1. <a class="paper-download" href="cbse2012-futures.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="cbse2012-futures.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Learning from the Future of Component Repositories**.  <em>To appear in proceedings of CBSE 2012:
+ 1. <a class="paper-download" href="cbse2012-futures.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="cbse2012-futures.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/2304736.2304747" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Learning from the Future of Component Repositories**.  <em>In proceedings of CBSE 2012:
       <a href="http://cbse-conferences.org/2012/">15th International ACM
       SIGSOFT Symposium on Component Based Software
       Engineering</a>, Bertinoro, Italy, June 26-28, 2012.
       <a href="http://cbse-conferences.org/2012/">15th International ACM
       SIGSOFT Symposium on Component Based Software
       Engineering</a>, Bertinoro, Italy, June 26-28, 2012.
+      ISBN 978-1-4503-1345-2,
+      <a href="http://dl.acm.org/citation.cfm?doid=2304736.2304747">pp. 51-60</a>,
+      ACM 2012.
       <em>Award:</em> <a href="http://europe.acm.org/best-paper.html">Best
       Paper Award</a>.</em>
     [[!toggle id=id41 text="Abstract..."]] [[!toggleable id=id41 text="""
     *Abstract:* An important aspect of the quality assurance of large component repositories is the logical coherence of component metadata. We argue that it is possible to identify certain classes of such problems by checking relevant properties of the possible future repositories into which the current repository may evolve. In order to make a complete analysis of all possible futures effective however, one needs a way to construct a finite set of representatives of this infinite set of potential futures. We define a class of properties for which this can be done. We illustrate the practical usefulness of the approach with two quality assurance applications: (i) establishing the amount of "forced upgrades" induced by introducing new versions of existing components in a repository, and (ii) identifying outdated components that need to be upgraded in order to ever be installable in the future. For both applications we provide experience reports obtained on the Debian distribution.
     """]]
       <em>Award:</em> <a href="http://europe.acm.org/best-paper.html">Best
       Paper Award</a>.</em>
     [[!toggle id=id41 text="Abstract..."]] [[!toggleable id=id41 text="""
     *Abstract:* An important aspect of the quality assurance of large component repositories is the logical coherence of component metadata. We argue that it is possible to identify certain classes of such problems by checking relevant properties of the possible future repositories into which the current repository may evolve. In order to make a complete analysis of all possible futures effective however, one needs a way to construct a finite set of representatives of this infinite set of potential futures. We define a class of properties for which this can be done. We illustrate the practical usefulness of the approach with two quality assurance applications: (i) establishing the amount of "forced upgrades" induced by introducing new versions of existing components in a repository, and (ii) identifying outdated components that need to be upgraded in order to ever be installable in the future. For both applications we provide experience reports obtained on the Debian distribution.
     """]]
- 1. <a class="paper-download" href="cbse2011-mpm.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="cbse2011-mpm.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/2000229.2000255" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **MPM: a modular package manager**.  <em>In proceedings of CBSE 2011: <a href="http://cbse-conferences.org/2011/">14th International ACM SIGSOFT
+ 1. <a class="paper-download" href="cbse2011-mpm.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="cbse2011-mpm.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/2000229.2000255" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **MPM: a modular package manager**.  <em>In proceedings of CBSE 2011: <a href="http://cbse-conferences.org/2011/">14th International ACM SIGSOFT
       Symposium on Component Based Software Engineering</a>,
       Boulder, Colorado, USA, 21-23 June, 2011. ISBN
       Symposium on Component Based Software Engineering</a>,
       Boulder, Colorado, USA, 21-23 June, 2011. ISBN
-      978-1-4503-0723-9, pp. 179-188,
+      978-1-4503-0723-9,
+      <a href="http://dl.acm.org/citation.cfm?doid=2000229.2000255">pp. 179-188</a>,
       ACM 2011. <em>Award:</em> <a href="http://www.sigsoft.org/">ACM SIGSOFT</a> Distinguished Paper
       Award</em>
     [[!toggle id=id36 text="Abstract..."]] [[!toggleable id=id36 text="""
       ACM 2011. <em>Award:</em> <a href="http://www.sigsoft.org/">ACM SIGSOFT</a> Distinguished Paper
       Award</em>
     [[!toggle id=id36 text="Abstract..."]] [[!toggleable id=id36 text="""
-    *Abstract:* Software distributions in the FOSS world rely on so-called package managers for the installation and removal of packages on target machines. State-of-the-art package managers are monolithic in architecture, and each of them is hard-wired to an ad-hoc dependency solver implementing a customized heuristics. In this paper we propose a modular architecture allowing for pluggable dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, accept more expressive input languages, and can be easily adaptable to new platforms. We present a working prototype—called MPM—which has been implemented following the design advocated in this paper.
+    *Abstract:* Software distributions in the FOSS world rely on so-called package managers for the installation and removal of packages on target machines. State-of-the-art package managers are monolithic in architecture, and each of them is hard-wired to an ad-hoc dependency solver implementing a customized heuristics. In this paper we propose a modular architecture allowing for pluggable dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, accept more expressive input languages, and can be easily adaptable to new platforms. We present a working prototype, called MPM, which has been implemented following the design advocated in this paper.
     """]]
     """]]
- 1. <a class="paper-download" href="splc2010-fd-deps.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="splc2010-fd-deps.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-642-15579-6_40" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Feature Diagrams as Package Dependencies**.  <em>In proceedings of SPLC 2010: <a href="http://msr.uwaterloo.ca/msr2010/">14th International Software
+ 1. <a class="paper-download" href="splc2010-fd-deps.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="splc2010-fd-deps.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-642-15579-6_40" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Feature Diagrams as Package Dependencies**.  <em>In proceedings of SPLC 2010: <a href="http://splc2010.postech.ac.kr/">14th International Software
       Product Line Conference</a>, Jeju Island, South Korea, 13-17
       September 2010. LNCS <a href="http://www.springerlink.com/content/978-3-642-15578-9/contents/">6287</a>,
       ISBN 978-3-642-15578-9, <a href="http://www.springerlink.com/content/7534146613550207/">pp. 476-480</a>,
       Product Line Conference</a>, Jeju Island, South Korea, 13-17
       September 2010. LNCS <a href="http://www.springerlink.com/content/978-3-642-15578-9/contents/">6287</a>,
       ISBN 978-3-642-15578-9, <a href="http://www.springerlink.com/content/7534146613550207/">pp. 476-480</a>,
@@ -129,7 +166,7 @@ in reverse chronological order.
        Florida, USA.
       </em>
     [[!toggle id=id28 text="Abstract..."]] [[!toggleable id=id28 text="""
        Florida, USA.
       </em>
     [[!toggle id=id28 text="Abstract..."]] [[!toggleable id=id28 text="""
-    *Abstract:* Component-based systems often describe context requirements in terms of explicit inter-component dependencies. Studying large instances of such systems—such as free and open source software (FOSS) distributions—in terms of declared dependencies between packages is appealing. It is however also misleading when the language to express dependencies is as expressive as boolean formulae, which is often the case. In such settings, a more appropriate notion of component dependency exists: strong dependency. This paper introduces such notion as a first step towards modeling semantic, rather then syntactic, inter-component relationships. Furthermore, a notion of component sensitivity is derived from strong dependencies, with applications to quality assurance and to the evaluation of upgrade risks. An empirical study of strong dependencies and sensitivity is presented, in the context of one of the largest, freely available, component-based system.
+    *Abstract:* Component-based systems often describe context requirements in terms of explicit inter-component dependencies. Studying large instances of such systems, such as free and open source software (FOSS) distributions, in terms of declared dependencies between packages is appealing. It is however also misleading when the language to express dependencies is as expressive as boolean formulae, which is often the case. In such settings, a more appropriate notion of component dependency exists: strong dependency. This paper introduces such notion as a first step towards modeling semantic, rather then syntactic, inter-component relationships. Furthermore, a notion of component sensitivity is derived from strong dependencies, with applications to quality assurance and to the evaluation of upgrade risks. An empirical study of strong dependencies and sensitivity is presented, in the context of one of the largest, freely available, component-based system.
     """]]
  1. <a class="paper-download" href="enase2009-upgrade.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="enase2009-upgrade.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-642-14819-4_19" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.di.univaq.it/cicchetti">Antonio Cicchetti</a>, <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **A Model Driven Approach to Upgrade Package-Based Software Systems**.  <em>In proceedings of <a href="http://www.enase.org/">ENASE
       2009</a>: 4th international conference on Evaluation of Novel Aspects to
     """]]
  1. <a class="paper-download" href="enase2009-upgrade.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="enase2009-upgrade.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-642-14819-4_19" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.di.univaq.it/cicchetti">Antonio Cicchetti</a>, <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **A Model Driven Approach to Upgrade Package-Based Software Systems**.  <em>In proceedings of <a href="http://www.enase.org/">ENASE
       2009</a>: 4th international conference on Evaluation of Novel Aspects to
@@ -139,11 +176,11 @@ in reverse chronological order.
       262-276</a>, Springer-Verlag,
       2010.</em>
     [[!toggle id=id26 text="Abstract..."]] [[!toggleable id=id26 text="""
       262-276</a>, Springer-Verlag,
       2010.</em>
     [[!toggle id=id26 text="Abstract..."]] [[!toggleable id=id26 text="""
-    *Abstract:* Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades—the latter being the most challenging aspect to deal with—in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.
+    *Abstract:* Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades, the latter being the most challenging aspect to deal with, in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.
     """]]
  1. <a class="paper-download" href="sac09-manners.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sac09-manners.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1529282.1529422" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://www.cs.unibo.it/~rossi/">Davide Rossi</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Where are your Manners? Sharing Best Community Practices in the Web 2.0**.  <em>In proceedings of ACM SAC 2009: the <a href="http://www.acm.org/conferences/sac/sac2009/">24th Annual ACM
       Symposium on Applied Computing</a>. ISBN
     """]]
  1. <a class="paper-download" href="sac09-manners.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sac09-manners.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1529282.1529422" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://www.cs.unibo.it/~rossi/">Davide Rossi</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Where are your Manners? Sharing Best Community Practices in the Web 2.0**.  <em>In proceedings of ACM SAC 2009: the <a href="http://www.acm.org/conferences/sac/sac2009/">24th Annual ACM
       Symposium on Applied Computing</a>. ISBN
-      978-1-60558-166-8, <a href="http://portal.acm.org/citation.cfm?id=1529282.1529422&amp;coll=ACM&amp;dl=ACM&amp;type=series&amp;idx=SERIES179&amp;part=series&amp;WantType=Proceedings&amp;title=SAC">pp. 681-687</a></em>
+      978-1-60558-166-8, <a href="http://portal.acm.org/citation.cfm?id=1529282.1529422&amp;coll=ACM&amp;dl=ACM&amp;type=series&amp;idx=SERIES179&amp;part=series&amp;WantType=Proceedings&amp;title=SAC">pp. 681-687</a>, ACM.</em>
     [[!toggle id=id23 text="Abstract..."]] [[!toggleable id=id23 text="""
     *Abstract:* The Web 2.0 fosters the creation of communities by offering users a wide array of social software tools. But, while the success of these tools is based on their ability to support different interaction patterns among users by imposing as less limitations as possible, the communities they support are not free of rules (just think about the posting rules in a community forum or the editing rules in a thematic wiki). In this paper we propose a framework for the sharing of best community practices in the form of a (potentially rule-based) annotation layer that can be integrated with existing Web 2.0 community tools (with specific focus on wikis). This solution is characterized by minimal intrusiveness and plays nicely within the open spirit of the Web 2.0 by proving users with behavioral hints rather than by enforcing the strict adherence to a set of rules.
     """]]
     [[!toggle id=id23 text="Abstract..."]] [[!toggleable id=id23 text="""
     *Abstract:* The Web 2.0 fosters the creation of communities by offering users a wide array of social software tools. But, while the success of these tools is based on their ability to support different interaction patterns among users by imposing as less limitations as possible, the communities they support are not free of rules (just think about the posting rules in a community forum or the editing rules in a thematic wiki). In this paper we propose a framework for the sharing of best community practices in the form of a (potentially rule-based) annotation layer that can be integrated with existing Web 2.0 community tools (with specific focus on wikis). This solution is characterized by minimal intrusiveness and plays nicely within the open spirit of the Web 2.0 by proving users with behavioral hints rather than by enforcing the strict adherence to a set of rules.
     """]]
@@ -177,7 +214,7 @@ in reverse chronological order.
        18-32</a>, 2007.
       </em>
     [[!toggle id=id10 text="Abstract..."]] [[!toggleable id=id10 text="""
        18-32</a>, 2007.
       </em>
     [[!toggle id=id10 text="Abstract..."]] [[!toggleable id=id10 text="""
-    *Abstract:* Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based—as Coq—on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
+    *Abstract:* Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based, as Coq, on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
     """]]
  1. <a class="paper-download" href="notation.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="notation.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11812289_16" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.sti.uniurb.it/padovani/">Luca Padovani</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **From Notation to Semantics: There and Back Again**.  <em>
        In Proceedings of <a href="http://www.mkm-ig.org/meetings/mkm06/">MKM 2006</a>: The 5th
     """]]
  1. <a class="paper-download" href="notation.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="notation.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11812289_16" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.sti.uniurb.it/padovani/">Luca Padovani</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **From Notation to Semantics: There and Back Again**.  <em>
        In Proceedings of <a href="http://www.mkm-ig.org/meetings/mkm06/">MKM 2006</a>: The 5th
@@ -228,6 +265,14 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed workshops">international, peer-reviewed workshop proceedings</span>
 
 
 # <span title="international, peer-reviewed workshops">international, peer-reviewed workshop proceedings</span>
 
+ 1. <a class="paper-download" href="msr2012-conflicts.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="msr2012-conflicts.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1109/MSR.2012.6224274" title="Document Object Identifier">doi&gt;</a></span> <a href="http://staff.aist.go.jp/c.artho/">Cyrille Valentin Artho</a>, Kuniyasu Suzaki, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Why do software packages conflict?**.  <em>In proceedings of <a href="http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6220358">MSR
+      2012</a>: <a href="http://2012.msrconf.org/">9th IEEE Working Conference
+      on Mining Software Repositories</a>, co-located with <a href="http://www.icse2012.org/">ICSE 2012</a>,
+      IEEE, ISBN 978-1-4673-1760-3, <a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6224274">pp. 141-150</a>.
+      June 2-3, Zurich, Switzerland.</em>
+    [[!toggle id=id44 text="Abstract..."]] [[!toggleable id=id44 text="""
+    *Abstract:* Determining whether two or more packages cannot be installed together is an important issue in the quality assurance process of package-based distributions. Unfortunately, the sheer number of different configurations to test makes this task particularly challenging, and hundreds of such incompatibilities go undetected by the normal testing and distribution process until they are later reported by a user as bugs that we call "conflict defects". We performed an extensive case study of conflict defects extracted from the bug tracking systems of Debian and Red Hat. According to our results, conflict defects can be grouped into five main categories. We show that with more detailed package meta-data, about 30% of all conflict defects could be prevented relatively easily, while another 30% could be found by targeted testing of packages that share common resources or characteristics. These results allow us to make precise suggestions on how to prevent and detect conflict defects in the future.
+    """]]
  1. <a class="paper-download" href="lococo2011-conflicts.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="lococo2011-conflicts.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://staff.aist.go.jp/c.artho/">Cyrille Valentin Artho</a>, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, Kuniyasu Suzaki, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Sources of Inter-package Conflicts in Debian**.  <em>
        In proceedings of <a href="http://lococo.irill.org/2011/">LoCoCo 2011</a> International
        Workshop on Logics for Component Configuration, affiliated
  1. <a class="paper-download" href="lococo2011-conflicts.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="lococo2011-conflicts.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://staff.aist.go.jp/c.artho/">Cyrille Valentin Artho</a>, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, Kuniyasu Suzaki, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Sources of Inter-package Conflicts in Debian**.  <em>
        In proceedings of <a href="http://lococo.irill.org/2011/">LoCoCo 2011</a> International
        Workshop on Logics for Component Configuration, affiliated
@@ -245,7 +290,7 @@ in reverse chronological order.
     [[!toggle id=id33 text="Abstract..."]] [[!toggleable id=id33 text="""
     *Abstract:* FLOSS distributions like RedHat and Ubuntu require a lot more complex infrastructures than most other FLOSS projects. In the case of community-driven distributions like Debian, the development of such an infrastructure is often not very organized, leading to new data sources being added in an impromptu manner while hackers set up new services that gain acceptance in the community. Mixing and matching data is then harder than should be, albeit being badly needed for Quality Assurance and data mining. Massive refactoring and integration is not a viable solution either, due to the constraints imposed by the bazaar development model. This paper presents the Ultimate Debian Database (UDD), which is the countermeasure adopted by the Debian project to the above "data hell". UDD gathers data from various data sources into a single, central SQL database, turning Quality Assurance needs that could not be easily implemented before into simple SQL queries. The paper also discusses the customs that have contributed to the data hell, the lessons learnt while designing UDD, and its applications and potentialities for data mining on FLOSS distributions.
     """]]
     [[!toggle id=id33 text="Abstract..."]] [[!toggleable id=id33 text="""
     *Abstract:* FLOSS distributions like RedHat and Ubuntu require a lot more complex infrastructures than most other FLOSS projects. In the case of community-driven distributions like Debian, the development of such an infrastructure is often not very organized, leading to new data sources being added in an impromptu manner while hackers set up new services that gain acceptance in the community. Mixing and matching data is then harder than should be, albeit being badly needed for Quality Assurance and data mining. Massive refactoring and integration is not a viable solution either, due to the constraints imposed by the bazaar development model. This paper presents the Ultimate Debian Database (UDD), which is the countermeasure adopted by the Debian project to the above "data hell". UDD gathers data from various data sources into a single, central SQL database, turning Quality Assurance needs that could not be easily implemented before into simple SQL queries. The paper also discusses the customs that have contributed to the data hell, the lessons learnt while designing UDD, and its applications and potentialities for data mining on FLOSS distributions.
     """]]
- 1. <a class="paper-download" href="mooml-iwoce-2009.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mooml-iwoce-2009.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595806" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Expressing Advanced User preferences in Component Installation**.  <em>
+ 1. <a class="paper-download" href="mooml-iwoce-2009.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mooml-iwoce-2009.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595806" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Expressing Advanced User preferences in Component Installation**.  <em>
        In proceedings of <a href="http://www.iwoce.org">IWOCE
        2009</a>: International Workshop on Open Component
        Ecosystem, affiliated with <a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
        In proceedings of <a href="http://www.iwoce.org">IWOCE
        2009</a>: International Workshop on Open Component
        Ecosystem, affiliated with <a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
@@ -290,7 +335,7 @@ in reverse chronological order.
        5-7, 2006.
       </em>
     [[!toggle id=id13 text="Abstract..."]] [[!toggleable id=id13 text="""
        5-7, 2006.
       </em>
     [[!toggle id=id13 text="Abstract..."]] [[!toggleable id=id13 text="""
-    *Abstract:* In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints—which relate the content of elements to the presence and values of other attributes or elements—are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.
+    *Abstract:* In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints, which relate the content of elements to the presence and values of other attributes or elements, are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.
     """]]
  1. <a class="paper-download" href="tinycals.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="tinycals.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.entcs.2006.09.026" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Tinycals: Step by Step Tacticals**.  <em>
        In Proceedings of <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>:
     """]]
  1. <a class="paper-download" href="tinycals.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="tinycals.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.entcs.2006.09.026" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Tinycals: Step by Step Tacticals**.  <em>
        In Proceedings of <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>:
@@ -335,7 +380,7 @@ in reverse chronological order.
 
 # <span title="national, peer-reviewed journals">national, peer-reviewed journal articles</span>
 
 
 # <span title="national, peer-reviewed journals">national, peer-reviewed journal articles</span>
 
- 1. <a class="paper-download" href="studia11-dh-ocaml.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="studia11-dh-ocaml.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.jussieu.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In <a href="http://studia.complexica.net/">Studia
+ 1. <a class="paper-download" href="studia11-dh-ocaml.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="studia11-dh-ocaml.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.univ-paris-diderot.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In <a href="http://studia.complexica.net/">Studia
       Informatica Universalis</a>, Volume 9, Issue
       1, pp. 129-157. Hermann
       2011.</em>
       Informatica Universalis</a>, Volume 9, Issue
       1, pp. 129-157. Hermann
       2011.</em>
@@ -345,7 +390,7 @@ in reverse chronological order.
 
 # <span title="national, peer-reviewed conferences and workshops">national, peer-reviewed conference and workshop procedings</span>
 
 
 # <span title="national, peer-reviewed conferences and workshops">national, peer-reviewed conference and workshop procedings</span>
 
- 1. <a class="paper-download" href="jfla10-dh-ocaml.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jfla10-dh-ocaml.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.jussieu.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In proceedings of JFLA 2010: <a href="http://jfla.inria.fr/2010/">21st Journée Francophones des Langages
+ 1. <a class="paper-download" href="jfla10-dh-ocaml.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jfla10-dh-ocaml.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.univ-paris-diderot.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In proceedings of JFLA 2010: <a href="http://jfla.inria.fr/2010/">21st Journée Francophones des Langages
       Applicatifs</a>, pp. 29-54. 30/01-02/02/2010 -
       La Ciotat, France.</em>
     [[!toggle id=id32 text="Abstract..."]] [[!toggleable id=id32 text="""
       Applicatifs</a>, pp. 29-54. 30/01-02/02/2010 -
       La Ciotat, France.</em>
     [[!toggle id=id32 text="Abstract..."]] [[!toggleable id=id32 text="""
@@ -354,13 +399,29 @@ in reverse chronological order.
 
 # <span title="official research reports of research institutions">technical reports</span>
 
 
 # <span title="official research reports of research institutions">technical reports</span>
 
+ 1. <a class="paper-download" href="zephyrus-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="zephyrus-tr.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, Michaël Lienhardt, <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, Jakub Zwolakowski. **Optimal Provisioning in the Cloud**.  <em>
+       <a href="http://www.aeolus-project.org/"><institution>Aeolus
+       project</institution></a> <a href="http://hal.archives-ouvertes.fr/hal-00831455">technical
+       report</a>, 7 Juin 2013.
+      </em>
+    [[!toggle id=id48 text="Abstract..."]] [[!toggleable id=id48 text="""
+    *Abstract:* Complex distributed systems are classically assembled by deploying several existing software components to multiple servers. Building such systems is a challenging problem that requires a significant amount of problem solving as one must i) ensure that all inter-component dependencies are satisfied; ii) ensure that no conflicting components are deployed on the same machine; and iii) take into account replication and distribution to account for quality of service, or possible failure of some services. We propose a tool, Zephyrus, that automates to a great extent assembling complex distributed systems. Given i) a high level specification of the desired system architecture, ii) the set of available components and their requirements) and iii) the current state of the system, Zephyrus is able to generate a formal representation of the desired system, to place the components in an optimal manner on the available machines, and to interconnect them as needed.
+    """]]
+ 1. <a class="paper-download" href="icalp2013-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="icalp2013-tr.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.cs.unibo.it/~jmauro/">Jacopo Mauro</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, <a href="http://www.cs.unibo.it/~zavattar/">Gianluigi Zavattaro</a>. **Component reconfiguration in the presence of conflicts**.  <em>
+       <a href="http://www.aeolus-project.org/"><institution>Aeolus
+       project</institution></a> <a href="http://hal.archives-ouvertes.fr/hal-00816468">technical
+       report</a>, 22 Avril 2013.
+      </em>
+    [[!toggle id=id47 text="Abstract..."]] [[!toggleable id=id47 text="""
+    *Abstract:* Components are traditionally modeled as black-boxes equipped with interfaces that indicate provided/required ports and, often, also conflicts with other components that cannot coexist with them. In modern tools for automatic system management, components become grey-boxes that show relevant internal states and the possible actions that can be acted on the components to change such state during the deployment and reconfiguration phases. However, state-of-the-art tools in this field do not support a systematic management of conflicts. In this paper we investigate the impact of conflicts by precisely characterizing the increment of complexity on the reconfiguration problem.
+    """]]
  1. <a class="paper-download" href="strongdeps-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="strongdeps-tr.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, Jaap Boender, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
        <a href="http://www.mancoosi.org/reports/">technical report
        0002</a>, 22/05/2009.
       </em>
     [[!toggle id=id27 text="Abstract..."]] [[!toggleable id=id27 text="""
  1. <a class="paper-download" href="strongdeps-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="strongdeps-tr.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, Jaap Boender, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
        <a href="http://www.mancoosi.org/reports/">technical report
        0002</a>, 22/05/2009.
       </em>
     [[!toggle id=id27 text="Abstract..."]] [[!toggleable id=id27 text="""
-    *Abstract:* Component-based systems often describe context requirements in terms of explicit inter-component dependencies. Studying large instances of such systems—such as free and open source software (FOSS) distributions—in terms of declared dependencies between packages is appealing. It is however also misleading when the language to express dependencies is as expressive as boolean formulae, which is often the case. In such settings, a more appropriate notion of component dependency exists: strong dependency. This paper introduces such notion as a first step towards modeling semantic, rather then syntactic, inter-component relationships. Furthermore, a notion of component sensitivity is derived from strong dependencies, with applications to quality assurance and to the evaluation of upgrade risks. An empirical study of strong dependencies and sensitivity is presented, in the context of one of the largest, freely available, component-based system.
+    *Abstract:* Component-based systems often describe context requirements in terms of explicit inter-component dependencies. Studying large instances of such systems, such as free and open source software (FOSS) distributions, in terms of declared dependencies between packages is appealing. It is however also misleading when the language to express dependencies is as expressive as boolean formulae, which is often the case. In such settings, a more appropriate notion of component dependency exists: strong dependency. This paper introduces such notion as a first step towards modeling semantic, rather then syntactic, inter-component relationships. Furthermore, a notion of component sensitivity is derived from strong dependencies, with applications to quality assurance and to the evaluation of upgrade risks. An empirical study of strong dependencies and sensitivity is presented, in the context of one of the largest, freely available, component-based system.
     """]]
  1. <a class="paper-download" href="mancoosi-d2.1.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mancoosi-d2.1.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Metamodel for Describing System Structure and State**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
     """]]
  1. <a class="paper-download" href="mancoosi-d2.1.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mancoosi-d2.1.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Metamodel for Describing System Structure and State**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
@@ -371,7 +432,7 @@ in reverse chronological order.
     [[!toggle id=id25 text="Abstract..."]] [[!toggleable id=id25 text="""
     *Abstract:* Today's software systems are very complex modular entities, made up of many interacting components that must be deployed and coexist in the same context. Modern operating systems provide the basic infrastructure for deploying and handling all the components that are used as the basic blocks for building more complex systems even though a generic and comprehensive support is far from being provided. In fact, in Free and Open Source Software (FOSS) systems, components evolve independently from each other and because of the huge amount of available components and their different project origins, it is not easy to manage the life cycle of a distribution. Users are in fact allowed to choose and install a wide variety of alternatives whose consistency cannot be checked a priori to their full extent. It is possible to easily make the system unusable by installing or removing some packages that "break" the consistency of what is installed in the system itself. This document proposes a model-driven approach to simulate system upgrades in advance and to detect predictable upgrade failures, possibly by notifying the user before the system is affected. The approach relies on an abstract representation of the systems and packages which are given in terms of models that are expressive enough to isolate inconsistent configurations (e.g., situations in which installed components rely on the presence of disappeared sub-components) that are currently not expressible as inter-package relationships.
     """]]
     [[!toggle id=id25 text="Abstract..."]] [[!toggleable id=id25 text="""
     *Abstract:* Today's software systems are very complex modular entities, made up of many interacting components that must be deployed and coexist in the same context. Modern operating systems provide the basic infrastructure for deploying and handling all the components that are used as the basic blocks for building more complex systems even though a generic and comprehensive support is far from being provided. In fact, in Free and Open Source Software (FOSS) systems, components evolve independently from each other and because of the huge amount of available components and their different project origins, it is not easy to manage the life cycle of a distribution. Users are in fact allowed to choose and install a wide variety of alternatives whose consistency cannot be checked a priori to their full extent. It is possible to easily make the system unusable by installing or removing some packages that "break" the consistency of what is installed in the system itself. This document proposes a model-driven approach to simulate system upgrades in advance and to detect predictable upgrade failures, possibly by notifying the user before the system is affected. The approach relies on an abstract representation of the systems and packages which are given in terms of models that are expressive enough to isolate inconsistent configurations (e.g., situations in which installed components rely on the presence of disappeared sub-components) that are currently not expressible as inter-package relationships.
     """]]
- 1. <a class="paper-download" href="mancoosi-d5.1.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mancoosi-d5.1.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Description of the CUDF Format**.  <em>
+ 1. <a class="paper-download" href="mancoosi-d5.1.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mancoosi-d5.1.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Description of the CUDF Format**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
        deliverable,
        <a href="http://www.mancoosi.org/deliverables/d5.1.pdf">D5.1</a>,
        <a href="http://www.mancoosi.org">Mancoosi project</a>
        deliverable,
        <a href="http://www.mancoosi.org/deliverables/d5.1.pdf">D5.1</a>,
@@ -392,7 +453,7 @@ in reverse chronological order.
          report UBLCS-2007-21</a>, August 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a>.
       </em>
     [[!toggle id=id16 text="Abstract..."]] [[!toggleable id=id16 text="""
          report UBLCS-2007-21</a>, August 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a>.
       </em>
     [[!toggle id=id16 text="Abstract..."]] [[!toggleable id=id16 text="""
-    *Abstract:* Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge—functional and creational templating—and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.
+    *Abstract:* Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge, functional and creational templating, and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.
     """]]
 
 # dissertations
     """]]
 
 # dissertations
@@ -405,7 +466,7 @@ in reverse chronological order.
          Miculan</a>).
       </em>
     [[!toggle id=id12 text="Abstract..."]] [[!toggleable id=id12 text="""
          Miculan</a>).
       </em>
     [[!toggle id=id12 text="Abstract..."]] [[!toggleable id=id12 text="""
-    *Abstract:* Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or "undo") past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathML-Presentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.
+    *Abstract:* Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant, Coq, with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or "undo") past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathML-Presentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.
     """]]
  1. <a class="paper-download" href="master-thesis.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="master-thesis.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)**.  <em>
        Master thesis (Italian only), March 2003, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a> (advisor: <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>; refereed
     """]]
  1. <a class="paper-download" href="master-thesis.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="master-thesis.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)**.  <em>
        Master thesis (Italian only), March 2003, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a> (advisor: <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>; refereed
@@ -414,7 +475,7 @@ in reverse chronological order.
 
 # miscellanea
 
 
 # miscellanea
 
- 1. <a class="paper-download" href="debconf8-mancoosi.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debconf8-mancoosi.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Solving package dependencies: from EDOS to Mancoosi**.  <em>In proceedings of <a href="http://debconf8.debconf.org/">DebConf8</a>: 9th annual conference
+ 1. <a class="paper-download" href="debconf8-mancoosi.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debconf8-mancoosi.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.pps.univ-paris-diderot.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Solving package dependencies: from EDOS to Mancoosi**.  <em>In proceedings of <a href="http://debconf8.debconf.org/">DebConf8</a>: 9th annual conference
       of the <a href="http://www.debian.org">Debian</a> project
       developers. August 10-16, 2008, Mar del Plata,
       Argentina.</em>
       of the <a href="http://www.debian.org">Debian</a> project
       developers. August 10-16, 2008, Mar del Plata,
       Argentina.</em>