This talk describes a recently started ANR project named Colis
(http://colis.irif.univ-paris-diderot.fr/), which has the goal of
developing techniques and tools for the formal verification of shell
scripts. More specifically, our goal is to verify the transformation
of a file system tree described by so-called debian maintainer
scripts. These scripts, often written in the Posix shell language, are
part of the software packages in the Debian GNU/Linux distribution.

A possible example of a program specification is absence of execution
error under certain initial conditions. Automatic program verification
even for this kind of specification is a challenging task. In case of
Debian maintainer scripts we are faced with even more challenging
properties like idempotency of scripts (required by policy), or
commutation of scripts.

The project is still in the beginning, so there are no results yet to
present. However, I will explain why I think that the case of Debian
maintainer scripts is very interesting for program verification : some
aspects of scripts (POSIX shell, manipulation of a complex data
structure) make the problem very difficult, while other aspects of the
Debian case are likely to make the problem easier than the task of
verifying any arbitary shell script.