papers: add two "to appear" entries
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 14 Jun 2012 13:07:08 +0000 (15:07 +0200)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 14 Jun 2012 13:07:08 +0000 (15:07 +0200)
research/publications.mdwn
research/publications/enase2009-upgrade.bib
research/publications/infsof2012-mpm.bib [new file with mode: 0644]
research/publications/matita-crafting.bib
research/publications/phd-thesis.bib
research/publications/sefm2012-aeolus.bib [new file with mode: 0644]
research/publications/streaming-co-constraints.bib
research/publications/wiki-templating-tr.bib

index d9a6cc9..7dcf580 100644 (file)
@@ -7,8 +7,13 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed journals">international, peer-reviewed journal articles</span>
 
+ 1. <a class="paper-download" href="infsof2012-mpm.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="infsof2012-mpm.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **A Modular Package Manager Architecture**.  <em>To appear in <a href="http://www.journals.elsevier.com/information-and-software-technology/">Information
+      and Software Technology</a>, Elsevier.</em>
+    [[!toggle id=id42 text="Abstract..."]] [[!toggleable id=id42 text="""
+    *Abstract:* The success of modern software distributions in the Free and Open Source world can be explained, among other factors, by the availability of a large collection of software packages and the possibility to easily install and remove those components using state of the art package managers. However, package managers are often built using a monolithic architecture and hard-wired and ad-hoc dependency solvers implementing some customized heuristics. In this paper we propose a modular architecture relying on precise interface formalisms that allows the system administrator to choose from a variety of dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, offer more expressive preference languages, and be easily adaptable to new platforms. We have built a working prototype—called MPM—following the design advocated in this paper, and we show how it largely outperforms a variety of state of the art package managers.
+    """]]
  1. <a class="paper-download" href="jss2012-concern.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="jss2012-concern.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.jss.2012.02.018" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Dependency Solving: a Separate Concern in Component Evolution Management**.  <em>To appear in <a href="http://www.journals.elsevier.com/journal-of-systems-and-software/">Journal
-      of Systems and Software</a>.</em>
+      of Systems and Software</a>, Elsevier.</em>
     [[!toggle id=id40 text="Abstract..."]] [[!toggleable id=id40 text="""
     *Abstract:* Maintenance of component-based software platforms often has to face rapid evolution of software components. Component dependencies, conflicts, and package managers with dependency solving capabilities are the key ingredients of prevalent software maintenance technologies that have been proposed to keep software installations synchronized with evolving component repositories. We review state-of-the-art package managers and their ability to keep up with evolution at the current growth rate of popular component-based platforms, and conclude that their dependency solving abilities are not up to the task. We show that the complexity of the underlying upgrade planning problem is NP-complete even for seemingly simple component models, and argue that the principal source of complexity lies in multiple available versions of components. We then discuss the need of expressive languages for user preferences, which makes the problem even more challenging. We propose to establish dependency solving as a separate concern from other upgrade aspects, and present CUDF as a formalism to describe upgrade scenarios. By analyzing the result of an international dependency solving competition, we provide evidence that the proposed approach is viable.
     """]]
@@ -52,8 +57,8 @@ in reverse chronological order.
        Automated Reasoning</a>, <a href="http://springerlink.metapress.com/content/h81468706x24/">Volume
        39, Number 2</a>. Springer
        Netherlands, <a href="http://www.springerlink.com/content/0168-7433">ISSN
-       0168-7433</a>, <a href="http://springerlink.metapress.com/content/y4wt440q28136q47">pp. 109-139</a>,
-       2007.
+       0168-7433</a>, <a href="http://springerlink.metapress.com/content/y4wt440q28136q47">pp.
+       109-139</a>, 2007.
       </em>
     [[!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.
@@ -75,6 +80,12 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed conferences">international, peer-reviewed conference proceedings</span>
 
+ 1. <a class="paper-download" href="sefm2012-aeolus.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sefm2012-aeolus.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>, <a href="http://www.cs.unibo.it/~zavattar/">Gianluigi Zavattaro</a>. **Towards a Formal Component Model for the Cloud**.  <em>To appear in proceedings of SEFM 2012: <a href="http://sefm2012.city.academic.gr/">10th International Conference on
+      Software Engineering and Formal Methods</a>, Thessaloniki,
+      Greece, 1-5 October, 2012.</em>
+    [[!toggle id=id43 text="Abstract..."]] [[!toggleable id=id43 text="""
+    *Abstract:* We consider the problem of deploying and (re)configuring resources in a "cloud" setting, where interconnected software components and services can be deployed on clusters of heterogeneous (virtual) machines that can be created and connected on-the-fly. We introduce the Aeolus component model to capture similar scenarii from realistic cloud deployments, and instrument automated planning of day-to-day activities such as software upgrade planning, service deployment, elastic scaling, etc. We formalize the model and characterize the feasibility and complexity of configuration achievability in Aeolus.
+    """]]
  1. <a class="paper-download" href="cbse2012-futures.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="cbse2012-futures.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Learning from the Future of Component Repositories**.  <em>To appear in proceedings of CBSE 2012:
       <a href="http://cbse-conferences.org/2012/">15th International ACM
       SIGSOFT Symposium on Component Based Software
@@ -126,7 +137,7 @@ in reverse chronological order.
       262-276</a>, Springer-Verlag,
       2010.</em>
     [[!toggle id=id26 text="Abstract..."]] [[!toggleable id=id26 text="""
-    *Abstract:* Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades---the latter being the most challenging aspect to deal with---in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.
+    *Abstract:* Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades—the latter being the most challenging aspect to deal with—in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.
     """]]
  1. <a class="paper-download" href="sac09-manners.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="sac09-manners.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1529282.1529422" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://www.cs.unibo.it/~rossi/">Davide Rossi</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Where are your Manners? Sharing Best Community Practices in the Web 2.0**.  <em>In proceedings of ACM SAC 2009: the <a href="http://www.acm.org/conferences/sac/sac2009/">24th Annual ACM
       Symposium on Applied Computing</a>. ISBN
@@ -164,7 +175,7 @@ in reverse chronological order.
        18-32</a>, 2007.
       </em>
     [[!toggle id=id10 text="Abstract..."]] [[!toggleable id=id10 text="""
-    *Abstract:* Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based---as Coq---on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
+    *Abstract:* Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based—as Coq—on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
     """]]
  1. <a class="paper-download" href="notation.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="notation.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11812289_16" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.sti.uniurb.it/padovani/">Luca Padovani</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **From Notation to Semantics: There and Back Again**.  <em>
        In Proceedings of <a href="http://www.mkm-ig.org/meetings/mkm06/">MKM 2006</a>: The 5th
@@ -275,7 +286,7 @@ in reverse chronological order.
        5-7, 2006.
       </em>
     [[!toggle id=id13 text="Abstract..."]] [[!toggleable id=id13 text="""
-    *Abstract:* In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints---which relate the content of elements to the presence and values of other attributes or elements---are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.
+    *Abstract:* In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints—which relate the content of elements to the presence and values of other attributes or elements—are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.
     """]]
  1. <a class="paper-download" href="tinycals.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="tinycals.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.entcs.2006.09.026" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Tinycals: Step by Step Tacticals**.  <em>
        In Proceedings of <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>:
@@ -312,8 +323,7 @@ in reverse chronological order.
        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.
+       88-7999-545-6, pp. 43-57, 2003.
       </em>
     [[!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).
@@ -378,7 +388,7 @@ in reverse chronological order.
          report UBLCS-2007-21</a>, August 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a>.
       </em>
     [[!toggle id=id16 text="Abstract..."]] [[!toggleable id=id16 text="""
-    *Abstract:* Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge---functional and creational templating---and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.
+    *Abstract:* Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge—functional and creational templating—and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.
     """]]
 
 # dissertations
@@ -391,7 +401,7 @@ in reverse chronological order.
          Miculan</a>).
       </em>
     [[!toggle id=id12 text="Abstract..."]] [[!toggleable id=id12 text="""
-    *Abstract:* Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant---Coq---with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or "undo") past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathML-Presentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.
+    *Abstract:* Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or "undo") past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathML-Presentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.
     """]]
  1. <a class="paper-download" href="master-thesis.pdf" title="download paper in PDF format">[.pdf]</a> <a class="bibtex-download" href="master-thesis.bib" title="download bibliographic entry in BibTeX format">[.bib]</a> <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)**.  <em>
        Master thesis (Italian only), March 2003, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a> (advisor: <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>; refereed
index addbff8..52fb563 100644 (file)
@@ -1,7 +1,7 @@
 @inproceedings{enase2009-upgrade,
   author = {Antonio Cicchetti and Di Ruscio, Davide and Patrizio Pelliccione and Alfonso Pierantonio and Stefano Zacchiroli},
   title = {A Model Driven Approach to Upgrade Package-Based Software Systems},
-  abstract = {Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades---the latter being the most challenging aspect to deal with---in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.},
+  abstract = {Complex software systems are more and more based on the abstraction of package, brought to popularity by Free and Open Source Software (FOSS) distributions. While helpful as an encapsulation layer, packages do not solve all problems of deployment, and more generally of management, of large software collections. In particular upgrades, which often affect several packages at once due to inter-package dependencies, often fail and do not hold good transactional properties. This paper shows how to apply model driven techniques to describe and manage software upgrades of FOSS distributions. It is discussed how to model static and dynamic aspects of package upgrades—the latter being the most challenging aspect to deal with—in order to be able to predict common causes of upgrade failures and undo residual effects of failed or undesired upgrades.},
   publisher = {Springer-Verlag},
   year = {2010},
   doi = {10.1007/978-3-642-14819-4_19},
diff --git a/research/publications/infsof2012-mpm.bib b/research/publications/infsof2012-mpm.bib
new file mode 100644 (file)
index 0000000..e8c08a9
--- /dev/null
@@ -0,0 +1,7 @@
+@article{infsof2012-mpm,
+  author = {Pietro Abate and Di Cosmo, Roberto and Ralf Treinen and Stefano Zacchiroli},
+  title = {A Modular Package Manager Architecture},
+  abstract = {The success of modern software distributions in the Free and Open Source world can be explained, among other factors, by the availability of a large collection of software packages and the possibility to easily install and remove those components using state of the art package managers. However, package managers are often built using a monolithic architecture and hard-wired and ad-hoc dependency solvers implementing some customized heuristics. In this paper we propose a modular architecture relying on precise interface formalisms that allows the system administrator to choose from a variety of dependency solvers and backends. We argue that this is the path that leads to the next generation of package managers that will deliver better results, offer more expressive preference languages, and be easily adaptable to new platforms. We have built a working prototype—called MPM—following the design advocated in this paper, and we show how it largely outperforms a variety of state of the art package managers.},
+  year = {2012},
+  journal = {Information and Software Technology},
+}
index 8c9b719..8d09078 100644 (file)
@@ -1,7 +1,7 @@
 @inproceedings{matita-crafting,
   author = {Andrea Asperti and Sacerdoti Coen, Claudio and Enrico Tassi and Stefano Zacchiroli},
   title = {Crafting a Proof Assistant},
-  abstract = {Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based---as Coq---on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.},
+  abstract = {Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based—as Coq—on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.},
   publisher = {Springer Berlin / Heidelberg},
   year = {2007},
   isbn = {978-3-540-74463-4},
index 9853ce5..143790f 100644 (file)
@@ -1,6 +1,6 @@
 @thesis{phd-thesis,
   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.},
+  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.},
   year = {2007},
 }
diff --git a/research/publications/sefm2012-aeolus.bib b/research/publications/sefm2012-aeolus.bib
new file mode 100644 (file)
index 0000000..7d58a3e
--- /dev/null
@@ -0,0 +1,7 @@
+@inproceedings{sefm2012-aeolus,
+  author = {Di Cosmo, Roberto and Stefano Zacchiroli and Zavattaro, Gianluigi},
+  title = {Towards a Formal Component Model for the Cloud},
+  abstract = {We consider the problem of deploying and (re)configuring resources in a "cloud" setting, where interconnected software components and services can be deployed on clusters of heterogeneous (virtual) machines that can be created and connected on-the-fly. We introduce the Aeolus component model to capture similar scenarii from realistic cloud deployments, and instrument automated planning of day-to-day activities such as software upgrade planning, service deployment, elastic scaling, etc. We formalize the model and characterize the feasibility and complexity of configuration achievability in Aeolus.},
+  year = {2012},
+  booktitle = {SEFM 2012: 10th International Conference on Software Engineering and Formal Methods},
+}
index 7fa894a..b43aea5 100644 (file)
@@ -1,7 +1,7 @@
 @inproceedings{streaming-co-constraints,
   author = {Paolo Marinelli and Stefano Zacchiroli},
   title = {Co-Constraint Validation in a Streaming Context},
-  abstract = {In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints---which relate the content of elements to the presence and values of other attributes or elements---are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.},
+  abstract = {In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints—which relate the content of elements to the presence and values of other attributes or elements—are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.},
   year = {2006},
   booktitle = {XML 2006: The world's oldest and biggest XML conference},
 }
index dd8e682..698815d 100644 (file)
@@ -1,6 +1,6 @@
 @techreport{wiki-templating-tr,
   author = {Di Iorio, Angelo and Fabio Vitali and Stefano Zacchiroli},
   title = {Templating Wiki Content for Fun and Profit},
-  abstract = {Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge---functional and creational templating---and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.},
+  abstract = {Content templating enables reuse of content structures between wiki pages. Such a feature is implemented in several mainstream wiki engines. Systematic study of its conceptual models and comparison of the available implementations are unfortunately missing in the wiki literature. In this paper we aim to fill this gap first analyzing template-related user needs, and then reviewing existing approaches at content templating. Our investigation shows that two models emerge—functional and creational templating—and that both have weakness failing to properly fit in "The Wiki Way". As a solution, we propose the adoption of creational templates enriched with light constraints, showing that such a solution has a low implementative footprint in state-of-the-art wiki engines, and that it has a synergy with semantic wikis.},
   year = {2007},
 }