A formal study of Free Software distributions

Over the last two decades, free and open source software has grown considerably. Distributions that started out with a few hundred packages now contain tens of thousands of packages, taken from many different sources. This creates problems for quality assurance. The tools and procedures used are no longer suitable for the size and complexity of modem distributions. In this thesis, we start by presenting a mathematical model of the commonalities between the different types of distributions (Debian and RPM) ; notably the concept of packages and the relations between them : dependencies and conflicts. The model is partially formalised using the Coq proof assistant. The model will subsequently be used to propose 'semantic' relations, more appropriate than existing relations for finding and correcting errors in distributions. We will also present algorithms that can be used to efficiently compute these relations, and we will use Coq to formally prove key theorems used by these algorithms Finally, we have validated our algorithms on existing distributions. We will present an analysis that is a result of this validation, as well as a discussion of the 'small world' phenomenon in relation with open source distributions.

Data and Resources

Additional Info

Field Value
Source https://theses.hal.science/tel-00698622
Author Boender, Jaap
Maintainer CCSD
Last Updated May 18, 2026, 09:29 (UTC)
Created May 18, 2026, 09:29 (UTC)
Identifier NNT: 2011PA077019
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
creator Boender, Jaap
date 2011-03-24T00:00:00
harvest_object_id 23764e8c-d45c-40d7-b8d7-e2ec0a55bb20
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-08-20T00:00:00
set_spec type:THESE