add papers: concur 2015, icsoc 2015, msr 2015
authorStefano Zacchiroli <>
Tue, 25 Aug 2015 09:54:45 +0000 (11:54 +0200)
committerStefano Zacchiroli <>
Tue, 25 Aug 2015 09:54:45 +0000 (11:54 +0200)
research/publications/aeolus-concur-2015.bib [new file with mode: 0644]
research/publications/aeolus-concur-2015.pdf [new file with mode: 0644]
research/publications/aeolus-icsoc-2015.bib [new file with mode: 0644]
research/publications/aeolus-icsoc-2015.pdf [new file with mode: 0644]

index aca4049..69847ad 100644 (file)
@@ -63,34 +63,34 @@ You might also be interested in my author profiles on
     *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="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Paolo Marinelli</a>, <a href="">Fabio Vitali</a>, <a href="">Stefano Zacchiroli</a>. **Towards the unification of formats for overlapping markup**.  <em>
-       In <a href="">New Review
-       of Hypermedia and Multimedia</a>, <a href="">Volume
-       14</a>, <a href="">Issue
-       1</a>, January 2008, <a href="">pp. 57-94</a>.
-       <a href="">Taylor and Francis</a>,
-       <a href="">ISSN
-       1361-4568</a>.
+        In <a href="">New Review
+        of Hypermedia and Multimedia</a>, <a href="">Volume
+        14</a>, <a href="">Issue
+        1</a>, January 2008, <a href="">pp. 57-94</a>.
+        <a href="">Taylor and Francis</a>,
+        <a href="">ISSN
+        1361-4568</a>.
     [[!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.
  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="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Claudio Sacerdoti Coen</a>, <a href="">Stefano Zacchiroli</a>. **Spurious Disambiguation Errors and How to Get Rid of Them**.  <em>
-       In <a href="">Mathematics in
-       Computer Science</a>, Volume 2, Number
-       2, <a href="">pp. 355-378</a>,
-       December 2008. Springer Birkhäuser,
-       <a href="">ISSN 1661-8270</a>.
+        In <a href="">Mathematics in
+        Computer Science</a>, Volume 2, Number
+        2, <a href="">pp. 355-378</a>,
+        December 2008. Springer Birkhäuser,
+        <a href="">ISSN 1661-8270</a>.
     [[!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.
  1. <a class="paper-download" href="matita.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="matita.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Andrea Asperti</a>, <a href="">Claudio Sacerdoti Coen</a>, <a href="">Enrico Tassi</a>, <a href="">Stefano Zacchiroli</a>. **User Interaction with the Matita Proof Assistant**.  <em>
-       In <a href="">Journal of
-       Automated Reasoning</a>, <a href="">Volume
-       39, Number 2</a>. Springer
-       Netherlands, <a href="">ISSN
-       0168-7433</a>, <a href="">pp.
-       109-139</a>, 2007.
+        In <a href="">Journal of
+        Automated Reasoning</a>, <a href="">Volume
+        39, Number 2</a>. Springer
+        Netherlands, <a href="">ISSN
+        0168-7433</a>, <a href="">pp.
+        109-139</a>, 2007.
     [[!toggle id=id9 text="Abstract..."]] [[!toggleable id=id9 text="""
     *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.
@@ -117,12 +117,12 @@ You might also be interested in my author profiles on
 # 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="">Angelo Di Iorio</a>, <a href="">Fabio Vitali</a>, <a href="">Stefano Zacchiroli</a>. **Web Semantics via Wiki Templating**.  <em>
-       Chapter 34 of <a href="">Handbook
-       of research on Web 2.0, 3.0 and x.0: technologies, business and social
-       applications</a>. San Murugesan Ed.,
-       Information Science Reference,
-       November 2009, ISBN
-       978-1605663845.
+        Chapter 34 of <a href="">Handbook
+        of research on Web 2.0, 3.0 and x.0: technologies, business and social
+        applications</a>. San Murugesan Ed.,
+        Information Science Reference,
+        November 2009, ISBN
+        978-1605663845.
     [[!toggle id=id21 text="Abstract..."]] [[!toggleable id=id21 text="""
     *Abstract:* A foreseeable incarnation of Web 3.0 could inherit machine understandability from the Semantic Web, and collaborative editing from Web 2.0 applications. We review the research and development trends which are getting today Web nearer to such an incarnation. We present semantic wikis, microformats, and the so-called "lowercase semantic web": they are the main approaches at closing the technological gap between content authors and Semantic Web technologies. We discuss a too often neglected aspect of the associated technologies, namely how much they adhere to the wiki philosophy of open editing: is there an intrinsic incompatibility between semantic rich content and unconstrained editing? We argue that the answer to this question can be "no", provided that a few yet relevant shortcomings of current Web technologies will be fixed soon.
@@ -130,35 +130,56 @@ You might also be interested in my author profiles on
 # <span title="international, peer-reviewed conferences">international, peer-reviewed conference proceedings</span>
- 1. <a class="paper-download" href="debsources-msr-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debsources-msr-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Stefano Zacchiroli</a>. **The Debsources Dataset: Two Decades of Debian Source Code Metadata**.  <em>To appear in proceedings of <a href="">MSR 2015</a>: The 12th Working Conference
+ 1. <a class="paper-download" href="aeolus-icsoc-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="aeolus-icsoc-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Roberto Di Cosmo</a>, Antoine Eiche, <a href="">Jacopo Mauro</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Gianluigi Zavattaro</a>, <a href="">Jakub Zwolakowski</a>. **Automatic Deployment of Services in the Cloud with Aeolus Blender**.  <em>To appear in proceedings of <a href="">ICSOC 2015</a>: 13th International Conference on
+      Service Oriented Computing, November 16-19, 2015, Goa, India.
+      </em>
+    [[!toggle id=id61 text="Abstract..."]] [[!toggleable id=id61 text="""
+    *Abstract:* We present Aeolus Blender (Blender in the following), a software product for the automatic deployment and configuration of complex service-based, distributed software systems in the "cloud". By relying on a configuration optimiser and a deployment planner, Blender fully automates the deployment of real-life applications on OpenStack cloud deployments, by exploiting a knowledge base of software services provided by the Mandriva Armonic tool suite. The final deployment is guaranteed to satisfy not only user requirements and relevant software dependencies, but also to be optimal with respect to the number of used virtual machines.
+    """]]
+ 1. <a class="paper-download" href="aeolus-concur-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="aeolus-concur-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Roberto Di Cosmo</a>, <a href="">Michael Lienhardt</a>, <a href="">Jacopo Mauro</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Gianluigi Zavattaro</a>, <a href="">Jakub Zwolakowski</a>. **Automatic Application Deployment in the Cloud: from Practice to Theory and Back**.  <em>To appear in proceedings of <a href="">CONCUR 2015</a>: 26th
+      International Conference on Concurrency Theory,
+      September 1-4, 2015, Madrid, Spain.
+      </em>
+    [[!toggle id=id60 text="Abstract..."]] [[!toggleable id=id60 text="""
+    *Abstract:* The problem of deploying a complex software application has been formally investigated in previous work by means of the abstract component model named Aeolus. As the problem turned out to be undecidable, simplified versions of the model were investigated in which decidability was restored by introducing limitations on the ways components are described. In this paper, we take an opposite approach, and investigate the possibility to address a relaxed version of the deployment problem without limiting the expressiveness of the component model. We identify three problems to be solved in sequence: (i) the verification of the existence of a final configuration in which all the constraints imposed by the single components are satisfied, (ii) the generation of a concrete configuration satisfying such constraints, and (iii) the synthesis of a plan to reach such a configuration possibly going through intermediary configurations that violate the non-functional constraints.
+    """]]
+ 1. <a class="paper-download" href="debsources-msr-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debsources-msr-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Stefano Zacchiroli</a>. **The Debsources Dataset: Two Decades of Debian Source Code Metadata**.  <em>In proceedings of <a href="">MSR 2015</a>: The 12th Working Conference
       on Mining Software Repositories, May 16-17, 2015, Florence,
       Italy. Co-located with
-      <a href="">ICSE 2015</a>. 2015.</em>
+      <a href="">ICSE 2015</a>.
+      ISBN ISBN 978-0-7695-5594-2,
+      <a href="">pp. 466-469</a>,
+      IEEE 2015.
+      </em>
     [[!toggle id=id59 text="Abstract..."]] [[!toggleable id=id59 text="""
     *Abstract:* We present the Debsources Dataset: distribution metadata and source code metrics spanning two decades of Free and Open Source Software (FOSS) history, seen through the lens of the Debian distribution. Debsources is a software platform used to gather, search, and publish on the Web the full source code of the Debian operating system, as well as measures about it. A notable public instance of Debsources is available at; it includes both current and historical releases of Debian. Plugins to compute popular source code metrics (lines of code, defined symbols, disk usage) and other derived data (e.g., checksums) have been written, integrated, and run on all the source code available on The Debsources Dataset is a PostgreSQL database dump of metadata, as of February 10th, 2015. The dataset contains both Debian-specific metadata—e.g., which software packages are available in which release, which source code file belong to which package, release dates, etc.—and source code information gathered by running Debsources plugins. The Debsources Dataset offer a very long-term historical view of the macro-level evolution and constitution of FOSS through the lens of popular, representative FOSS projects of their times.
- 1. <a class="paper-download" href="distcheck-msr-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="distcheck-msr-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Pietro Abate</a>, <a href="">Roberto Di Cosmo</a>, <a href="">Louis Gesbert</a>, <a href="">Fabrice Le Fessant</a>, <a href="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>. **Mining Component Repositories for Installability Issues**.  <em>To appear in proceedings of <a href="">MSR 2015</a>: The 12th Working Conference
+ 1. <a class="paper-download" href="distcheck-msr-2015.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="distcheck-msr-2015.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Pietro Abate</a>, <a href="">Roberto Di Cosmo</a>, <a href="">Louis Gesbert</a>, <a href="">Fabrice Le Fessant</a>, <a href="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>. **Mining Component Repositories for Installability Issues**.  <em>In proceedings of <a href="">MSR 2015</a>: The 12th Working Conference
       on Mining Software Repositories, May 16-17, 2015, Florence,
       Italy. Co-located with
-      <a href="">ICSE 2015</a>. 2015.</em>
+      <a href="">ICSE 2015</a>.
+      ISBN ISBN 978-0-7695-5594-2,
+      <a href="">pp. 24-33</a>,
+      IEEE 2015.
+      </em>
     [[!toggle id=id58 text="Abstract..."]] [[!toggleable id=id58 text="""
     *Abstract:* Component repositories play an increasingly relevant role in software life-cycle management, from software distribution to end-user, to deployment and upgrade management. Software components shipped via such repositories are equipped with rich metadata that describe their relationship (e.g., dependencies and conflicts) with other components. In this practice paper we show how to use a tool, distcheck, that uses component metadata to identify all the components in a repository that cannot be installed (e.g., due to unsatisfiable dependencies), provides detailed information to help developers understanding the cause of the problem, and fix it in the repository. We report about detailed analyses of several repositories: the Debian distribution, the OPAM package collection, and Drupal modules. In each case, distcheck is able to efficiently identify not installable components and provide valuable explanations of the issues. Our experience provides solid ground for generalizing the use of distcheck to other component repositories.
  1. <a class="paper-download" href="zephyrus-ase-2014.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="zephyrus-ase-2014.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Roberto Di Cosmo</a>, <a href="">Michael Lienhardt</a>, <a href="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Jakub Zwolakowski</a>, Antoine Eiche, Alexis Agahi. **Automated Synthesis and Deployment of Cloud Applications**.  <em>
-       In proceedings of <a href="">ASE
-       2014</a>: 29th IEEE/ACM International Conference on Automated Software
-       Engineering, September 15-19, 2014, Vasteras, Sweden. ISBN
-       978-1-4503-3013-8, <a href="">pp. 211-222</a>,
-       ACM 2014.
+        In proceedings of <a href="">ASE
+        2014</a>: 29th IEEE/ACM International Conference on Automated Software
+        Engineering, September 15-19, 2014, Vasteras, Sweden. ISBN
+        978-1-4503-3013-8, <a href="">pp. 211-222</a>,
+        ACM 2014.
     [[!toggle id=id54 text="Abstract..."]] [[!toggleable id=id54 text="""
     *Abstract:* Complex networked applications are assembled by connecting software components distributed across multiple machines. Building and deploying such systems is a challenging problem which requires a significant amount of expertise: the system architect must ensure that all component dependencies are satisfied, avoid conflicting components, and add the right amount of component replicas to account for quality of service and fault-tolerance. In a cloud environment, one also needs to minimize the virtual resources provisioned upfront, to reduce the cost of operation. Once the full architecture is designed, it is necessary to correctly orchestrate the deployment phase, to ensure all components are started and connected in the right order. We present a toolchain that automates the assembly and deployment of such complex distributed applications. Given as input a high-level specification of the desired system, the set of available components together with their requirements, and the maximal amount of virtual resources to be committed, it synthesizes the full architecture of the system, placing components in an optimal manner using the minimal number of available machines, and automatically deploys the complete system in a cloud environment.
  1. <a class="paper-download" href="debsources-esem-2014.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debsources-esem-2014.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Matthieu Caneill</a>, <a href="">Stefano Zacchiroli</a>. **Debsources: Live and Historical Views on Macro-Level Software Evolution**.  <em>
-       In proceedings of <a href="">ESEM 2014</a>: 8th
-       International Symposium on Empirical Software Engineering and
-       Measurement, September 18-19, 2014, Torino, Italy. ISBN <a href="">
-       978-1-4503-2774-9</a>, ACM 2014.
+        In proceedings of <a href="">ESEM 2014</a>: 8th
+        International Symposium on Empirical Software Engineering and
+        Measurement, September 18-19, 2014, Torino, Italy. ISBN <a href="">
+        978-1-4503-2774-9</a>, ACM 2014.
     [[!toggle id=id53 text="Abstract..."]] [[!toggleable id=id53 text="""
     *Abstract:* Context. Software evolution has been an active field of research in recent years, but studies on macro-level software evolution---i.e., on the evolution of large software collections over many years---are scarce, despite the increasing popularity of intermediate vendors as a way to deliver software to final users. Goal. We want to ease the study of both day-by-day and long-term Free and Open Source Software (FOSS) evolution trends at the macro-level, focusing on the Debian distribution as a proxy of relevant FOSS projects. Method. We have built Debsources, a software platform to gather, search, and publish on the Web all the source code of Debian and measures about it. We have set up a public Debsources instance at, integrated it into the Debian infrastructure to receive live updates of new package releases, and written plugins to compute popular source code metrics. We have injected all current and historical Debian releases into it. Results. The obtained dataset and Web portal provide both long term-views over the past 20 years of FOSS evolution and live insights on what is happening at sub-day granularity. By writing simple plugins (~100 lines of Python each) and adding them to our Debsources instance we have been able to easily replicate and extend past empirical analyses on metrics as diverse as lines of code, number of packages, and rate of change---and make them perennial. We have obtained slightly different results than our reference study, but confirmed the general trends and updated them in light of 7 extra years of evolution history. Conclusions. Debsources is a flexible platform to monitor large FOSS collections over long periods of time. Its main instance and dataset are valuable resources for scholars interested in macro-level software evolution.
@@ -254,11 +275,11 @@ You might also be interested in my author profiles on
     *Abstract:* Web office suites such as Google Docs offer unparalleled collaboration experiences in terms of low software requirements, ease of use, data ubiquity, and availability. When the data holder (Google, Microsoft, etc.) is not perceived as trusted though, those benefits are considered at stake with important privacy requirements. Content cloaking is a lightweight, cryptographic, client-side solution to protect content from data holders while using web office suites and other "Web 2.0", AJAX-based, collaborative applications.
  1. <a class="paper-download" href="strongdeps-esem-2009.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="strongdeps-esem-2009.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Pietro Abate</a>, Jaap Boender, <a href="">Roberto Di Cosmo</a>, <a href="">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em>
-       In proceedings of <a href="">ESEM 2009</a>: 3rd
-       International Symposium on Empirical Software Engineering and
-       Measurement, ISBN 978-1-4244-4842-5, <a href="">pp.
-       89-99</a>. October 15-16, 2009 - Lake Buena Vista,
-       Florida, USA.
+        In proceedings of <a href="">ESEM 2009</a>: 3rd
+        International Symposium on Empirical Software Engineering and
+        Measurement, ISBN 978-1-4244-4842-5, <a href="">pp.
+        89-99</a>. October 15-16, 2009 - Lake Buena Vista,
+        Florida, USA.
     [[!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.
@@ -280,79 +301,79 @@ You might also be interested in my author profiles on
     *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.
  1. <a class="paper-download" href="wiki-templating.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="wiki-templating.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Angelo Di Iorio</a>, <a href="">Fabio Vitali</a>, <a href="">Stefano Zacchiroli</a>. **Wiki Content Templating**.  <em>
-       In Proceedings of <a href="">WWW 2008</a>:
-       17th International World Wide Web Conference. April 21-25,
-       2008 Beijing, China. ACM ISBN
-       978-1-60558-085-2/08/04, <a href="">pp.
-       615-624</a>.
+        In Proceedings of <a href="">WWW 2008</a>:
+        17th International World Wide Web Conference. April 21-25,
+        2008 Beijing, China. ACM ISBN
+        978-1-60558-085-2/08/04, <a href="">pp.
+        615-624</a>.
     [[!toggle id=id18 text="Abstract..."]] [[!toggleable id=id18 text="""
     *Abstract:* Wiki content templating enables reuse of content structures among wiki pages. In this paper we present a thorough study of this widespread feature, showing how its two state of the art models (functional and creational templating) are sub-optimal. We then propose a third, better, model called lightly constrained (LC) templating and show its implementation in the Moin wiki engine. We also show how LC templating implementations are the appropriate technologies to push forward semantically rich web pages on the lines of (lowercase) semantic web and microformats.
  1. <a class="paper-download" href="disambiguation-errors.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="disambiguation-errors.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Claudio Sacerdoti Coen</a>, <a href="">Stefano Zacchiroli</a>. **Spurious Disambiguation Error Detection**.  <em>
-       In Proceedings of <a href="">MKM 2007</a>: The
-       6th International Conference on Mathematical Knowledge
-       Management.  Hagenberg, Austria -- 27-30 June 2007. <a href="">LNAI 4573</a>,
-       Springer Berlin / Heidelberg, ISBN
-       978-3-540-73083-5, <a href="">pp.
-       381-392</a>, 2007.
+        In Proceedings of <a href="">MKM 2007</a>: The
+        6th International Conference on Mathematical Knowledge
+        Management.  Hagenberg, Austria -- 27-30 June 2007. <a href="">LNAI 4573</a>,
+        Springer Berlin / Heidelberg, ISBN
+        978-3-540-73083-5, <a href="">pp.
+        381-392</a>, 2007.
     [[!toggle id=id14 text="Abstract..."]] [[!toggleable id=id14 text="""
     *Abstract:* The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae we want to present only errors related to the interpretation meant by the user, hiding errors related to other interpretations (spurious errors). We propose a heuristic to recognize spurious errors, which has been integrated with the disambiguation algorithm of [1].
  1. <a class="paper-download" href="matita-crafting.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="matita-crafting.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Andrea Asperti</a>, <a href="">Claudio Sacerdoti Coen</a>, <a href="">Enrico Tassi</a>, <a href="">Stefano Zacchiroli</a>. **Crafting a Proof Assistant**.  <em>
-       In Proceedings of <a href="">Types 2006</a>: Types for
-       Proofs and Programs. Nottingham, UK -- April 18-21, 2006.
-       LNCS <a href="">4502</a>,
-       Springer Berlin / Heidelberg, ISBN
-       978-3-540-74463-4, <a href="">pp.
-       18-32</a>, 2007.
+        In Proceedings of <a href="">Types 2006</a>: Types for
+        Proofs and Programs. Nottingham, UK -- April 18-21, 2006.
+        LNCS <a href="">4502</a>,
+        Springer Berlin / Heidelberg, ISBN
+        978-3-540-74463-4, <a href="">pp.
+        18-32</a>, 2007.
     [[!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.
  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="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Luca Padovani</a>, <a href="">Stefano Zacchiroli</a>. **From Notation to Semantics: There and Back Again**.  <em>
-       In Proceedings of <a href="">MKM 2006</a>: The 5th
-       International Conference on Mathematical Knowledge
-       Management.  Wokingham, UK -- August 11-12, 2006. <a href="">LNAI
-       4108</a>, Springer Berlin / Heidelberg, ISBN
-       978-3-540-37104-5, <a href="">pp.
-       194-207</a>, 2006.
+        In Proceedings of <a href="">MKM 2006</a>: The 5th
+        International Conference on Mathematical Knowledge
+        Management.  Wokingham, UK -- August 11-12, 2006. <a href="">LNAI
+        4108</a>, Springer Berlin / Heidelberg, ISBN
+        978-3-540-37104-5, <a href="">pp.
+        194-207</a>, 2006.
     [[!toggle id=id6 text="Abstract..."]] [[!toggleable id=id6 text="""
     *Abstract:* Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully. In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications.
  1. <a class="paper-download" href="whelp.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="whelp.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Andrea Asperti</a>, <a href="">Ferruccio Guidi</a>, <a href="">Claudio Sacerdoti Coen</a>, <a href="">Enrico Tassi</a>, <a href="">Stefano Zacchiroli</a>. **A Content Based Mathematical Search Engine: Whelp**.  <em>
-       In Proceedings of <a href="">TYPES
-       2004</a>: Types for Proofs and Programs. Paris, France --
-       December 15-18, 2004. LNCS <a href="">3839</a>,
-       Springer Berlin / Heidelberg, ISBN
-       3-540-31428-8, <a href="">pp.
-       17-32</a>, 2006.
+        In Proceedings of <a href="">TYPES
+        2004</a>: Types for Proofs and Programs. Paris, France --
+        December 15-18, 2004. LNCS <a href="">3839</a>,
+        Springer Berlin / Heidelberg, ISBN
+        3-540-31428-8, <a href="">pp.
+        17-32</a>, 2006.
     [[!toggle id=id5 text="Abstract..."]] [[!toggleable id=id5 text="""
     *Abstract:* The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The prototype, called Whelp, exploits a metadata approach for indexing the information that looks far more flexible than traditional indexing techniques for structured expressions like substitution, discrimination, or context trees. The prototype has been instantiated to the standard library of the Coq proof assistant extended with many user contributions.
  1. <a class="paper-download" href="gmetadom.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="gmetadom.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Luca Padovani</a>, <a href="">Claudio Sacerdoti Coen</a>, <a href="">Stefano Zacchiroli</a>. **A Generative Approach to the Implementation of Language Bindings for the Document Object Model**.  <em>
-       In Proceedings of <a href="">GPCE'04</a> 3rd International Conference
-       on Generative Programming and Component
-       Engineering. Vancouver, Canada -- October 24-28, 2004 LNCS
-       <a href="">3286</a>,
-       Springer Berlin / Heidelberg, ISBN
-       3-540-23580-9, <a href="">pp.
-       469-487</a>, 2004.
+        In Proceedings of <a href="">GPCE'04</a> 3rd International Conference
+        on Generative Programming and Component
+        Engineering. Vancouver, Canada -- October 24-28, 2004 LNCS
+        <a href="">3286</a>,
+        Springer Berlin / Heidelberg, ISBN
+        3-540-23580-9, <a href="">pp.
+        469-487</a>, 2004.
     [[!toggle id=id4 text="Abstract..."]] [[!toggleable id=id4 text="""
     *Abstract:* The availability of a C implementation for the Document Object Model (DOM) gives the interesting opportunity of generating bindings for different programming languages automatically. Because of the DOM bias towards Java-like languages, a C implementation that fakes objects, inheritance, polymorphism, exceptions and uses reference-counting introduces a gap between the API specification and its actual implementation that the bindings should try to close. In this paper we overview the generative approach in this particular context and apply it for the generation of C++ and OCaml bindings.
  1. <a class="paper-download" href="disambiguation.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="disambiguation.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Claudio Sacerdoti Coen</a>, <a href="">Stefano Zacchiroli</a>. **Efficient Ambiguous Parsing of Mathematical Formulae**.  <em>
-       In Proceedings of <a href="">MKM 2004</a>: 3rd
-       International Conference on Mathematical Knowledge
-       Management. September 19-21, 2004 Bialowieza - Poland.
-       LNCS <a href="">3119</a>,
-       Springer Berlin / Heidelberg, ISBN
-       3-540-23029-7, <a href="">pp.
-       347-362</a>, 2004.
+        In Proceedings of <a href="">MKM 2004</a>: 3rd
+        International Conference on Mathematical Knowledge
+        Management. September 19-21, 2004 Bialowieza - Poland.
+        LNCS <a href="">3119</a>,
+        Springer Berlin / Heidelberg, ISBN
+        3-540-23029-7, <a href="">pp.
+        347-362</a>, 2004.
     [[!toggle id=id2 text="Abstract..."]] [[!toggleable id=id2 text="""
     *Abstract:* Mathematical notation has the characteristic of being ambiguous: operators can be overloaded and information that can be deduced is often omitted. Mathematicians are used to this ambiguity and can easily disambiguate a formula making use of the context and of their ability to find the right interpretation. Software applications that have to deal with formulae usually avoid these issues by fixing an unambiguous input notation. This solution is annoying for mathematicians because of the resulting tricky syntaxes and becomes a show stopper to the simultaneous adoption of tools characterized by different input languages. In this paper we present an efficient algorithm suitable for ambiguous parsing of mathematical formulae. The only requirement of the algorithm is the existence of a validity predicate over abstract syntax trees of incomplete formulae with placeholders. This requirement can be easily fulfilled in the applicative area of interactive proof assistants, and in several other areas of Mathematical Knowledge Management.
@@ -367,31 +388,31 @@ You might also be interested in my author profiles on
     *Abstract:* Determining whether some components can be installed on a system is a complex problem: not only it is NP-complete in the worst case, but there can also be exponentially many solutions to it. Ordinary package managers use ad-hoc heuristics to solve this installation problem and choose a particular solution, making extremely difficult to change or sidestep these heuristics when the result is not the one we expect. When software repositories become complex enough, one gets vastly superior results by delegating dependency handling to a specialised solver, and use optimisation functions (or preferences) to control the class of solutions that are found. The opam package manager relies on the CUDF pivot format, which allows OCaml users that have a CUDF-compliant solver on their machine to reap the benefits of preferences-based dependency resolution. Thanks to the solver farm provided by Irill, these benefits are now extended to the OCaml community at large. In this talk we will present the preferences language and explain how to use it.
  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="">Cyrille Valentin Artho</a>, <a href="">Roberto Di Cosmo</a>, Kuniyasu Suzaki, <a href="">Stefano Zacchiroli</a>. **Sources of Inter-package Conflicts in Debian**.  <em>
-       In proceedings of <a href="">LoCoCo 2011</a> International
-       Workshop on Logics for Component Configuration, affiliated
-       with <a href="">CP 2011</a>
+        In proceedings of <a href="">LoCoCo 2011</a> International
+        Workshop on Logics for Component Configuration, affiliated
+        with <a href="">CP 2011</a>
     [[!toggle id=id38 text="Abstract..."]] [[!toggleable id=id38 text="""
     *Abstract:* Inter-package conflicts require the presence of two or more packages in a particular configuration, and thus tend to be harder to detect and localize than conventional (intra-package) defects. Hundreds of such inter-package conflicts go undetected by the normal testing and distribution process until they are later reported by a user. The reason for this is that current meta-data is not fine-grained and accurate enough to cover all common types of conflicts. A case study of inter-package conflicts in Debian has shown that with more detailed package meta-data, at least one third of all package conflicts could be prevented relatively easily, while another one third could be found by targeted testing of packages that share common resources or characteristics. This paper reports the case study and proposes ideas to detect inter-package conflicts in the future.
  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="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>. **Expressing Advanced User preferences in Component Installation**.  <em>
-       In proceedings of <a href="">IWOCE
-       2009</a>: International Workshop on Open Component
-       Ecosystem, affiliated with <a href="">ESEC/FSE
-       2009</a>. Foundations of Software Engineering, ISBN
-       978-1-60558-677-9, <a href="">pp. 31-40</a>,
-       ACM 2009.
+        In proceedings of <a href="">IWOCE
+        2009</a>: International Workshop on Open Component
+        Ecosystem, affiliated with <a href="">ESEC/FSE
+        2009</a>. Foundations of Software Engineering, ISBN
+        978-1-60558-677-9, <a href="">pp. 31-40</a>,
+        ACM 2009.
     [[!toggle id=id30 text="Abstract..."]] [[!toggleable id=id30 text="""
     *Abstract:* State of the art component-based software collections, such as FOSS distributions, are made of up to dozens of thousands components, with complex inter-dependencies and conflicts. Given a particular installation of such a system, each request to alter the set of installed components has potentially (too) many satisfying answers. We present an architecture that allows to express advanced user preferences about package selection in FOSS distributions. The architecture is composed by a distribution-independent format for describing available and installed packages called CUDF (Common Upgradeability Description Format), and a foundational language called MooML to specify optimization criteria. We present the syntax and semantics of CUDF and MooML, and discuss the partial evaluation mechanism of MooML which allows to gain efficiency in package dependency solvers.
  1. <a class="paper-download" href="modernization-iwoce-2009.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="modernization-iwoce-2009.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Davide Di Ruscio</a>, <a href="">Patrizio Pelliccione</a>, <a href="">Alfonso Pierantonio</a>, <a href="">Stefano Zacchiroli</a>. **Towards maintainer script modernization in FOSS distributions**.  <em>
-       In proceedings of <a href="">IWOCE
-       2009</a>: International Workshop on Open Component
-       Ecosystem, affiliated with <a href="">ESEC/FSE
-       2009</a>. Foundations of Software Engineering, ISBN
-       978-1-60558-677-9, <a href="">pp. 11-20</a>,
-       ACM 2009.
+        In proceedings of <a href="">IWOCE
+        2009</a>: International Workshop on Open Component
+        Ecosystem, affiliated with <a href="">ESEC/FSE
+        2009</a>. Foundations of Software Engineering, ISBN
+        978-1-60558-677-9, <a href="">pp. 11-20</a>,
+        ACM 2009.
     [[!toggle id=id29 text="Abstract..."]] [[!toggleable id=id29 text="""
     *Abstract:* Free and Open Source Software (FOSS) distributions are complex software systems, made of thousands packages that evolve rapidly, independently, and without centralized coordination. During packages upgrades, corner case failures can be encountered and are hard to deal with, especially when they are due to misbehaving maintainer scripts: executable code snippets used to finalize package configuration. In this paper we report a software modernization experience, the process of representing existing legacy systems in terms of models, applied to FOSS distributions. We present a process to define meta-models that enable dealing with upgrade failures and help rolling back from them, taking into account maintainer scripts. The process has been applied to widely used FOSS distributions and we report about such experiences.
@@ -404,59 +425,59 @@ You might also be interested in my author profiles on
     *Abstract:* The upgrade problems faced by Free and Open Source Software distributions have characteristics not easily found elsewhere. We describe the structure of packages and their role in the upgrade process. We show that state of the art package managers have shortcomings inhibiting their ability to cope with frequent upgrade failures. We survey current countermeasures to such failures, argue that they are not satisfactory, and sketch alternative solutions.
  1. <a class="paper-download" href="steve-latvia.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="steve-latvia.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Paolo Marinelli</a>, <a href="">Fabio Vitali</a>, <a href="">Stefano Zacchiroli</a>. **Streaming Validation of Schemata: the Lazy Typing Discipline**.  <em>
-       In Proceedings of <a href="">Extreme Markup
-       Languages 2007</a>: The Markup Theory and Practice
-       Conference. August 7-10, 2007 Montreal, Canada.
+        In Proceedings of <a href="">Extreme Markup
+        Languages 2007</a>: The Markup Theory and Practice
+        Conference. August 7-10, 2007 Montreal, Canada.
     [[!toggle id=id15 text="Abstract..."]] [[!toggleable id=id15 text="""
     *Abstract:* Assertions, identity constraints, and conditional type assignments are (planned) features of XML Schema which rely on XPath evaluation to various ends. The allowed XPath subset exploitable in those features is trimmed down for streamability concerns partly understandable (the apparent wish to avoid buffering to determine the evaluation of an expression) and partly artificial. In this paper we dissect the XPath language in subsets with varying streamability characteristics. We also identify the larger subset which is compatible with the typing discipline we believe underlies some of the choices currently present in the XML Schema specifications. We describe such a discipline as imposing that the type of an element has to be decided when its start tag is encountered and its validity has to be when its end tag is. We also propose an alternative lazy typing discipline where both type assignment and validity assessment are fired as soon as they are available in a best effort manner. We believe our discipline is more flexible and delegate to schema authors the choice of where to place in the trade-off between using larger XPath subsets and increasing buffering requirements or expeditiousness of typing information availability.
  1. <a class="paper-download" href="streaming-co-constraints.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="streaming-co-constraints.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Paolo Marinelli</a>, <a href="">Stefano Zacchiroli</a>. **Co-Constraint Validation in a Streaming Context**.  <em>
-       In Proceedings of <a href="">XML 2006</a>: The world's oldest
-       and biggest XML conference. <em>Award</em>: Winner of the
-       <a href="">XML
-       Scholarship 2006</a> as best student paper.  Boston, MA -- December
-       5-7, 2006.
+        In Proceedings of <a href="">XML 2006</a>: The world's oldest
+        and biggest XML conference. <em>Award</em>: Winner of the
+        <a href="">XML
+        Scholarship 2006</a> as best student paper.  Boston, MA -- December
+        5-7, 2006.
     [[!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.
  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="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Claudio Sacerdoti Coen</a>, <a href="">Enrico Tassi</a>, <a href="">Stefano Zacchiroli</a>. **Tinycals: Step by Step Tacticals**.  <em>
-       In Proceedings of <a href="">UITP 2006</a>:
-       User Interfaces for Theorem Provers. Seattle, WA -- August
-       21, 2006. <a href="">ENTCS
-       (Elsevier, ISSN 1571-0661)</a>, <a href="">Volume
-       174, Issue 2,
-       pp. 125-142. May 2007</a>.
+        In Proceedings of <a href="">UITP 2006</a>:
+        User Interfaces for Theorem Provers. Seattle, WA -- August
+        21, 2006. <a href="">ENTCS
+        (Elsevier, ISSN 1571-0661)</a>, <a href="">Volume
+        174, Issue 2,
+        pp. 125-142. May 2007</a>.
     [[!toggle id=id8 text="Abstract..."]] [[!toggleable id=id8 text="""
     *Abstract:* Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.
  1. <a class="paper-download" href="constrainedwiki.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="constrainedwiki.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> <a href="">Angelo Di Iorio</a>, <a href="">Stefano Zacchiroli</a>. **Constrained Wiki: an Oxymoron?**.  <em>
-       In Proceedings of <a href="">WikiSym 2006</a>: the 2006
-       International Symposium on Wikis. Odense, Denmark -- August
-       21-23, 2006.  ACM, 2006, ISBN
-       1-59593-417-0, <a href="">pp.
-       89-98</a>.
+        In Proceedings of <a href="">WikiSym 2006</a>: the 2006
+        International Symposium on Wikis. Odense, Denmark -- August
+        21-23, 2006.  ACM, 2006, ISBN
+        1-59593-417-0, <a href="">pp.
+        89-98</a>.
     [[!toggle id=id7 text="Abstract..."]] [[!toggleable id=id7 text="""
     *Abstract:* In this paper we propose a new wiki concept -- light constraints -- designed to encode community best practices and domain-specific requirements, and to assist in their application. While the idea of constraining user editing of wiki content seems to inherently contradict "The Wiki Way", it is well-known that communities of users involved in wiki sites have the habit of establishing best authoring practices. For domain-specific wiki systems which process wiki content, it is often useful to enforce some well-formedness conditions on specific page contents. This paper describes a general framework to think about the interaction of wiki system with constraints, and presents a generic architecture which can be easily incorporated into existing wiki systems to exploit the capabilities enabled by light constraints.
  1. <a class="paper-download" href="mathsearch.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="mathsearch.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Andrea Asperti</a>, <a href="">Stefano Zacchiroli</a>. **Searching Mathematics on the Web: State of the Art and Future Developments**.  <em>
-       In Proceedings of <a href="">New Developments in
-       Electronic Publishing AMS/SMM</a> Special Session, Houston,
-       May 2004 ECM4 Satellite Conference, Stockholm, June 2004 <a href="">pp. 9-18</a>.
-       FIZ Karlsruhe, ISBN 3-88127-107-4.
+        In Proceedings of <a href="">New Developments in
+        Electronic Publishing AMS/SMM</a> Special Session, Houston,
+        May 2004 ECM4 Satellite Conference, Stockholm, June 2004 <a href="">pp. 9-18</a>.
+        FIZ Karlsruhe, ISBN 3-88127-107-4.
     [[!toggle id=id3 text="Abstract..."]] [[!toggleable id=id3 text="""
     *Abstract:* A huge amount of mathematical knowledge is nowadays available on the World Wide Web. Many different solutions and technologies for searching that knowledge have been developed as well. We present the state of the art of searching mathematics on the Web, giving some insight on future developments in this area.
  1. <a class="paper-download" href="hbugs.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="hbugs.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Claudio Sacerdoti Coen</a>, <a href="">Stefano Zacchiroli</a>. **Brokers and Web-Services for Automatic Deduction: a Case Study**.  <em>
-       In Proceedings of <a href="">Calculemus 2003</a>:
-       11th Symposium on the Integration of Symbolic Computation and
-       Mechanized Reasoning. Roma, Italy -- September 10-12, 2003,
-       Aracne Editrice. ISBN
-       88-7999-545-6, pp. 43-57, 2003.
+        In Proceedings of <a href="">Calculemus 2003</a>:
+        11th Symposium on the Integration of Symbolic Computation and
+        Mechanized Reasoning. Roma, Italy -- September 10-12, 2003,
+        Aracne Editrice. ISBN
+        88-7999-545-6, pp. 43-57, 2003.
     [[!toggle id=id1 text="Abstract..."]] [[!toggleable id=id1 text="""
     *Abstract:* We present a planning broker and several Web-Services for automatic deduction. Each Web-Service implements one of the tactics usually available in interactive proof-assistants. When the broker is submitted a proof status (an incomplete proof tree and a focus on an open goal) it dispatches the proof to the Web-Services, collects the successful results, and send them back to the client as hints as soon as they are available. In our experience this architecture turns out to be helpful both for experienced users (who can take benefit of distributing heavy computations) and beginners (who can learn from it).
@@ -484,57 +505,57 @@ You might also be interested in my author profiles on
 # <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="">Roberto Di Cosmo</a>, <a href="">Michael Lienhardt</a>, <a href="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Jakub Zwolakowski</a>. **Optimal Provisioning in the Cloud**.  <em>
-       <a href="">Aeolus
-       project</a> <a href="">technical
-       report</a>, 7 Juin 2013.
+        <a href="">Aeolus
+        project</a> <a href="">technical
+        report</a>, 7 Juin 2013.
     [[!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="">Roberto Di Cosmo</a>, <a href="">Jacopo Mauro</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Gianluigi Zavattaro</a>. **Component reconfiguration in the presence of conflicts**.  <em>
-       <a href="">Aeolus
-       project</a> <a href="">technical
-       report</a>, 22 Avril 2013.
+        <a href="">Aeolus
+        project</a> <a href="">technical
+        report</a>, 22 Avril 2013.
     [[!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> <a href="">Pietro Abate</a>, Jaap Boender, <a href="">Roberto Di Cosmo</a>, <a href="">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em>
-       <a href="">Mancoosi project</a>
-       <a href="">technical report
-       0002</a>, 22 May 2009.
+        <a href="">Mancoosi project</a>
+        <a href="">technical report
+        0002</a>, 22 May 2009.
     [[!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.
  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="">Davide Di Ruscio</a>, <a href="">Patrizio Pelliccione</a>, <a href="">Alfonso Pierantonio</a>, <a href="">Stefano Zacchiroli</a>. **Metamodel for Describing System Structure and State**.  <em>
-       <a href="">Mancoosi project</a>
-       deliverable,
-       <a href="">D2.1</a>,
-       work package 2. January 2009.
+        <a href="">Mancoosi project</a>
+        deliverable,
+        <a href="">D2.1</a>,
+        work package 2. January 2009.
     [[!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="">Ralf Treinen</a>, <a href="">Stefano Zacchiroli</a>. **Description of the CUDF Format**.  <em>
-       <a href="">Mancoosi project</a>
-       deliverable,
-       <a href="">D5.1</a>,
-       work package 5. November 2008.
+        <a href="">Mancoosi project</a>
+        deliverable,
+        <a href="">D5.1</a>,
+        work package 5. November 2008.
     [[!toggle id=id24 text="Abstract..."]] [[!toggleable id=id24 text="""
     *Abstract:* This document contains several related specifications, taken together they describe the document formats related to the solver competition which will be organized by Mancoosi. In particular, this document describes: DUDF (Distribution Upgradeability Description Format), the document format to be used to submit upgrade problem instances from user machines to a (distribution-specific) database of upgrade problems; CUDF (Common Upgradeability Description Format), the document format used to encode upgrade problems, abstracting over distribution-specific details. Solvers taking part in the competition will be fed with input in CUDF format.
  1. <a class="paper-download" href="flea.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="flea.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Luca Padovani</a>, <a href="">Stefano Zacchiroli</a>. **Stream Processing of XML Documents Made Easy with LALR(1) Parser Generators**.  <em>
-       <a href="">Technical
-         report UBLCS-2007-23</a>, September 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a>.
+        <a href="">Technical
+          report UBLCS-2007-23</a>, September 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a>.
     [[!toggle id=id17 text="Abstract..."]] [[!toggleable id=id17 text="""
     *Abstract:* Because of their fully annotated structure, XML documents are normally believed to require a straightforward parsing phase. However, the standard APIs for accessing their content (the Document Object Model and the Simple API for XML) provide a programming interface that is very low-level and is thus inadequate for the recognition of any structure that is not isomorphic to its XML encoding. Even when the document undergoes validation, its unmarshalling into application-specific data using these APIs requires poorly maintainable, tedious-to-write, and possibly inefficient code. We describe a technique for the simultaneous parsing, validation, and unmarshalling of XML documents that combines a stream-oriented XML parser with a LALR(1) parser in order to guarantee efficient stream processing, expressive validation capabilities, and the possibility to associate user-provided actions with specific patterns occurring in the source documents.
  1. <a class="paper-download" href="wiki-templating-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="wiki-templating-tr.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Angelo Di Iorio</a>, <a href="">Fabio Vitali</a>, <a href="">Stefano Zacchiroli</a>. **Templating Wiki Content for Fun and Profit**.  <em>
-       <a href="">Technical
-         report UBLCS-2007-21</a>, August 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a>.
+        <a href="">Technical
+          report UBLCS-2007-21</a>, August 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a>.
     [[!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.
@@ -543,18 +564,18 @@ You might also be interested in my author profiles on
 # dissertations
  1. <a class="paper-download" href="phd-thesis.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="phd-thesis.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Stefano Zacchiroli</a>. **User Interaction Widgets for Interactive Theorem Proving**.  <em>
-       Ph.D. dissertation, <a href="">Technical
-         report UBLCS-2007-10</a>, March 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a> (advisor: <a href="">Andrea Asperti</a>; refereed
-       by: <a href="">Christoph
-         Benzmueller</a>, <a href="">Marino
-         Miculan</a>).
+        Ph.D. dissertation, <a href="">Technical
+          report UBLCS-2007-10</a>, March 2007, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a> (advisor: <a href="">Andrea Asperti</a>; refereed
+        by: <a href="">Christoph
+          Benzmueller</a>, <a href="">Marino
+          Miculan</a>).
     [[!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.
  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="">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="">Department of Computer Science</a>, <a href="">University of Bologna</a> (advisor: <a href="">Andrea Asperti</a>; refereed
-       by: <a href="">Nadia Busi</a>).
+        Master thesis (Italian only), March 2003, <a href="">Department of Computer Science</a>, <a href="">University of Bologna</a> (advisor: <a href="">Andrea Asperti</a>; refereed
+        by: <a href="">Nadia Busi</a>).
diff --git a/research/publications/aeolus-concur-2015.bib b/research/publications/aeolus-concur-2015.bib
new file mode 100644 (file)
index 0000000..a562311
--- /dev/null
@@ -0,0 +1,7 @@
+  author = {Di Cosmo, Roberto and Lienhardt, Michael and Mauro, Jacopo and Stefano Zacchiroli and Zavattaro, Gianluigi and Zwolakowski, Jakub},
+  title = {Automatic Application Deployment in the Cloud: from Practice to Theory and Back},
+  abstract = {The problem of deploying a complex software application has been formally investigated in previous work by means of the abstract component model named Aeolus. As the problem turned out to be undecidable, simplified versions of the model were investigated in which decidability was restored by introducing limitations on the ways components are described. In this paper, we take an opposite approach, and investigate the possibility to address a relaxed version of the deployment problem without limiting the expressiveness of the component model. We identify three problems to be solved in sequence: (i) the verification of the existence of a final configuration in which all the constraints imposed by the single components are satisfied, (ii) the generation of a concrete configuration satisfying such constraints, and (iii) the synthesis of a plan to reach such a configuration possibly going through intermediary configurations that violate the non-functional constraints.},
+  year = {2015},
+  booktitle = {CONCUR 2015: 26th International Conference on Concurrency Theory},
diff --git a/research/publications/aeolus-concur-2015.pdf b/research/publications/aeolus-concur-2015.pdf
new file mode 100644 (file)
index 0000000..38d4b27
Binary files /dev/null and b/research/publications/aeolus-concur-2015.pdf differ
diff --git a/research/publications/aeolus-icsoc-2015.bib b/research/publications/aeolus-icsoc-2015.bib
new file mode 100644 (file)
index 0000000..ef0924a
--- /dev/null
@@ -0,0 +1,7 @@
+  author = {Di Cosmo, Roberto and Antoine Eiche and Mauro, Jacopo and Stefano Zacchiroli and Zavattaro, Gianluigi and Zwolakowski, Jakub},
+  title = {Automatic Deployment of Services in the Cloud with Aeolus Blender},
+  abstract = {We present Aeolus Blender (Blender in the following), a software product for the automatic deployment and configuration of complex service-based, distributed software systems in the "cloud". By relying on a configuration optimiser and a deployment planner, Blender fully automates the deployment of real-life applications on OpenStack cloud deployments, by exploiting a knowledge base of software services provided by the Mandriva Armonic tool suite. The final deployment is guaranteed to satisfy not only user requirements and relevant software dependencies, but also to be optimal with respect to the number of used virtual machines.},
+  year = {2015},
+  booktitle = {ICSOC 2015: 13th International Conference on Service Oriented Computing},
diff --git a/research/publications/aeolus-icsoc-2015.pdf b/research/publications/aeolus-icsoc-2015.pdf
new file mode 100644 (file)
index 0000000..865fd62
Binary files /dev/null and b/research/publications/aeolus-icsoc-2015.pdf differ
index 6bea166..152b291 100644 (file)
@@ -2,6 +2,10 @@
   author = {Stefano Zacchiroli},
   title = {The Debsources Dataset: Two Decades of Debian Source Code Metadata},
   abstract = {We present the Debsources Dataset: distribution metadata and source code metrics spanning two decades of Free and Open Source Software (FOSS) history, seen through the lens of the Debian distribution. Debsources is a software platform used to gather, search, and publish on the Web the full source code of the Debian operating system, as well as measures about it. A notable public instance of Debsources is available at; it includes both current and historical releases of Debian. Plugins to compute popular source code metrics (lines of code, defined symbols, disk usage) and other derived data (e.g., checksums) have been written, integrated, and run on all the source code available on The Debsources Dataset is a PostgreSQL database dump of metadata, as of February 10th, 2015. The dataset contains both Debian-specific metadata—e.g., which software packages are available in which release, which source code file belong to which package, release dates, etc.—and source code information gathered by running Debsources plugins. The Debsources Dataset offer a very long-term historical view of the macro-level evolution and constitution of FOSS through the lens of popular, representative FOSS projects of their times.},
+  publisher = {IEEE},
   year = {2015},
+  isbn = {ISBN 978-0-7695-5594-2},
+  doi = {10.1109/MSR.2015.65},
+  pages = {466-469},
   booktitle = {MSR 2015: The 12th Working Conference on Mining Software Repositories},
index 3ad57d7..5a49ed2 100644 (file)
@@ -2,6 +2,10 @@
   author = {Pietro Abate and Di Cosmo, Roberto and Louis Gesbert and Fabrice Le Fessant and Ralf Treinen and Stefano Zacchiroli},
   title = {Mining Component Repositories for Installability Issues},
   abstract = {Component repositories play an increasingly relevant role in software life-cycle management, from software distribution to end-user, to deployment and upgrade management. Software components shipped via such repositories are equipped with rich metadata that describe their relationship (e.g., dependencies and conflicts) with other components. In this practice paper we show how to use a tool, distcheck, that uses component metadata to identify all the components in a repository that cannot be installed (e.g., due to unsatisfiable dependencies), provides detailed information to help developers understanding the cause of the problem, and fix it in the repository. We report about detailed analyses of several repositories: the Debian distribution, the OPAM package collection, and Drupal modules. In each case, distcheck is able to efficiently identify not installable components and provide valuable explanations of the issues. Our experience provides solid ground for generalizing the use of distcheck to other component repositories.},
+  publisher = {IEEE},
   year = {2015},
+  isbn = {ISBN 978-0-7695-5594-2},
+  doi = {10.1109/MSR.2015.10},
+  pages = {24-33},
   booktitle = {MSR 2015: The 12th Working Conference on Mining Software Repositories},