add recent publications and biblio info
authorStefano Zacchiroli <>
Tue, 6 Jun 2017 08:20:38 +0000 (10:20 +0200)
committerStefano Zacchiroli <>
Tue, 6 Jun 2017 08:20:38 +0000 (10:20 +0200)
research/publications/aeolus-blender-tr.bib [new file with mode: 0644]
research/publications/aeolus-blender-tr.pdf [new file with mode: 0644]
research/publications/oss-2017-proceedings.bib [new file with mode: 0644]
research/publications/oss-2017-proceedings.pdf [new file with mode: 0644]

index fe85f02..945514b 100644 (file)
@@ -13,9 +13,14 @@ You might also be interested in my author profiles on
 # <span title="international, peer-reviewed journals">international, peer-reviewed journal articles</span>
- 1. <a class="paper-download" href="debsources-ese-2016.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debsources-ese-2016.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="">Daniel M. Germán</a>, <a href="">Stefano Zacchiroli</a>. **The Debsources Dataset: Two Decades of Free and Open Source Software**.  <em>To appear in <a href="">Empirical Software
-      Engineering</a>. 2016.
-      ISSN 1382-3256, Springer.</em>
+ 1. <a class="paper-download" href="debsources-ese-2016.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="debsources-ese-2016.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="">Daniel M. Germán</a>, <a href="">Stefano Zacchiroli</a>. **The Debsources Dataset: Two Decades of Free and Open Source Software**.  <em>
+       In <a href="">Empirical Software
+       Engineering</a>,
+       Volume 22,
+       <a href="">pp. 1405-1437</a>,
+       June, 2017.
+       ISSN 1382-3256, Springer.
+      </em>
     [[!toggle id=id62 text="Abstract..."]] [[!toggleable id=id62 text="""
     *Abstract:* We present the Debsources Dataset: source code and related metadata spanning two decades of Free and Open Source Software (FOSS) history, seen through the lens of the Debian distribution. The dataset spans more than 3 billion lines of source code as well as metadata about them such as: size metrics (lines of code, disk usage), developer-defined symbols (ctags), file-level checksums (SHA1, SHA256, TLSH), file media types (MIME), release information (which version of which package containing which source code files has been released when), and license information (GPL, BSD, etc). The Debsources Dataset comes as a set of tarballs containing deduplicated unique source code files organized by their SHA1 checksums (the source code), plus a portable PostgreSQL database dump (the metadata). A case study is run to show how the Debsources Dataset can be used to easily and efficiently instrument very long-term analyses of the evolution of Debian from various angles (size, granularity, licensing, etc.), getting a grasp of major FOSS trends of the past two decades. The Debsources Dataset is Open Data, released under the terms of the CC BY-SA 4.0 license, and available for download from Zenodo with DOI reference 10.5281/zenodo.61089.
@@ -104,6 +109,13 @@ You might also be interested in my author profiles on
 # editorials
+ 1. <a class="paper-download" href="oss-2017-proceedings.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="oss-2017-proceedings.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="" title="Document Object Identifier">doi&gt;</a></span> Federico Balaguer, <a href="">Roberto Di Cosmo</a>, Alejandra Garrido, Fabio Kon, Gregorio Robles, <a href="">Stefano Zacchiroli</a>. **Open Source Systems: Towards Robust Practices**.  <em>
+       13th IFIP WG 2.13 International Conference, OSS 2017, Buenos Aires,
+       Argentina, May 22-23, 2017, Proceedings. IFIP
+       Advances in Information and Communication Technology
+       496, Springer
+       2017, ISBN 978-3-319-57734-0.
+      </em>
  1. <a class="paper-download" href="jwe-wt-2014-editorial.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jwe-wt-2014-editorial.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="">Angelo Di Iorio</a>, <a href="">Davide Rossi</a>, <a href="">Stefano Zacchiroli</a>. **Editorial**.  <em>In <a href="">Journal of Web
       Engineering</a>, Volume 14, Number 1-2,
       pp. 1-2.
@@ -517,6 +529,13 @@ 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="aeolus-blender-tr.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="aeolus-blender-tr.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="">Gianluigi Zavattaro</a>, <a href="">Stefano Zacchiroli</a>, <a href="">Jakub Zwolakowski</a>. **Automatic Deployment of Software Components in the Cloud with the Aeolus Blender**.  <em>
+       Inria <a href="">technical
+       report</a> 2015.
+      </em>
+    [[!toggle id=id63 text="Abstract..."]] [[!toggleable id=id63 text="""
+    *Abstract:* Cloud computing allows to build sophisticated software sys-tems on virtualized infrastructures at a fraction of the cost that was necessary just a few years ago. The deployment of such complex systems, though, is still a serious issue due to the need of deploying a large number of packages and services, their elaborated interdependencies, and the need to define the (ideally optimal) allocation of software compo-nents onto available computing resources. In this paper we present the Aeolus Blender (Blender in the following), a toolchain that automates the assembly and deployment of complex component-based software systems in the "cloud". By relying on a configuration optimizer and a deployment planner, Blender fully automates the deploy-ment of real-life cloud applications on OpenStack infrastruc-tures, by exploiting a knowledge base of software compo-nents defined in the Mandriva Armonic tool-suite. The final deployment is guaranteed to satisfy not only user require-ments and software dependencies, but also to be optimal with respect to the number of used virtual machines.
+    """]]
  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
diff --git a/research/publications/aeolus-blender-tr.bib b/research/publications/aeolus-blender-tr.bib
new file mode 100644 (file)
index 0000000..79108ab
--- /dev/null
@@ -0,0 +1,7 @@
+  author = {Di Cosmo, Roberto and Antoine Eiche and Mauro, Jacopo and Zavattaro, Gianluigi and Stefano Zacchiroli and Zwolakowski, Jakub},
+  title = {Automatic Deployment of Software Components in the Cloud with the Aeolus Blender},
+  abstract = {Cloud computing allows to build sophisticated software sys-tems on virtualized infrastructures at a fraction of the cost that was necessary just a few years ago. The deployment of such complex systems, though, is still a serious issue due to the need of deploying a large number of packages and services, their elaborated interdependencies, and the need to define the (ideally optimal) allocation of software compo-nents onto available computing resources. In this paper we present the Aeolus Blender (Blender in the following), a toolchain that automates the assembly and deployment of complex component-based software systems in the "cloud". By relying on a configuration optimizer and a deployment planner, Blender fully automates the deploy-ment of real-life cloud applications on OpenStack infrastruc-tures, by exploiting a knowledge base of software compo-nents defined in the Mandriva Armonic tool-suite. The final deployment is guaranteed to satisfy not only user require-ments and software dependencies, but also to be optimal with respect to the number of used virtual machines.},
+  year = {2015},
+  howpublished = {\url{}},
diff --git a/research/publications/aeolus-blender-tr.pdf b/research/publications/aeolus-blender-tr.pdf
new file mode 100644 (file)
index 0000000..ea03fb3
Binary files /dev/null and b/research/publications/aeolus-blender-tr.pdf differ
index 2f32d06..d7af6c6 100644 (file)
@@ -3,8 +3,11 @@
   title = {The Debsources Dataset: Two Decades of Free and Open Source Software},
   abstract = {We present the Debsources Dataset: source code and related metadata spanning two decades of Free and Open Source Software (FOSS) history, seen through the lens of the Debian distribution. The dataset spans more than 3 billion lines of source code as well as metadata about them such as: size metrics (lines of code, disk usage), developer-defined symbols (ctags), file-level checksums (SHA1, SHA256, TLSH), file media types (MIME), release information (which version of which package containing which source code files has been released when), and license information (GPL, BSD, etc). The Debsources Dataset comes as a set of tarballs containing deduplicated unique source code files organized by their SHA1 checksums (the source code), plus a portable PostgreSQL database dump (the metadata). A case study is run to show how the Debsources Dataset can be used to easily and efficiently instrument very long-term analyses of the evolution of Debian from various angles (size, granularity, licensing, etc.), getting a grasp of major FOSS trends of the past two decades. The Debsources Dataset is Open Data, released under the terms of the CC BY-SA 4.0 license, and available for download from Zenodo with DOI reference 10.5281/zenodo.61089.},
   publisher = {Springer},
-  year = {2016},
+  month = {June},
+  year = {2017},
   issn = {1382-3256},
   doi = {10.1007/s10664-016-9461-5},
+  pages = {1405-1437},
+  volume = {22},
   journal = {Empirical Software Engineering},
index 717449d..5d1d63f 100644 (file)
@@ -1,4 +1,4 @@
   author = {Stefano Zacchiroli},
   title = {Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)},
   abstract = {},
diff --git a/research/publications/oss-2017-proceedings.bib b/research/publications/oss-2017-proceedings.bib
new file mode 100644 (file)
index 0000000..d65cbbb
--- /dev/null
@@ -0,0 +1,12 @@
+  editor = {Federico Balaguer and Di Cosmo, Roberto and Alejandra Garrido and Fabio Kon and Gregorio Robles and Stefano Zacchiroli},
+  title = {Open Source Systems: Towards Robust Practices},
+  abstract = {},
+  publisher = {Springer},
+  month = {May},
+  year = {2017},
+  isbn = {978-3-319-57734-0},
+  doi = {10.1007/978-3-319-57735-7},
+  series = {IFIP Advances in Information and Communication Technology},
+  volume = {496},
diff --git a/research/publications/oss-2017-proceedings.pdf b/research/publications/oss-2017-proceedings.pdf
new file mode 100644 (file)
index 0000000..caa31ed
Binary files /dev/null and b/research/publications/oss-2017-proceedings.pdf differ
index 32fd4fa..53c00e5 100644 (file)
@@ -1,4 +1,4 @@
   author = {Stefano Zacchiroli},
   title = {User Interaction Widgets for Interactive Theorem Proving},
   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.},