********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle S16, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 16 juin 2006 10h30-12h00 ******************************* George Necula (Berkeley University, visiting ENS) Using Dependent Types for Low-Level Systems Programming Abstract: Types are recognized as a convenient specification mechanism, but simple types are not expressive enough to describe relationships between values, as necessary for low-level programming. For example, in low-level code using pointer arithmetic we must relate the value of the pointer with the variables that store the bounds of the enclosing array. We propose, Deputy, a lightweight specification mechanism based on dependent types for the C programming language. The novel feature over previous uses of dependent types is a mechanism for using them soundly in presence of pointers and mutation. We show that dependent types are a natural specification mechanism for enforcing common safe programming practices in existing C programs. Finally, we describe our experience using this mechanism to efficiently enforce memory safety for several Linux device drivers. *** Vendredi 16 juin 2006 14h00-15h30 ******************************* Alexey Gotsman (University of Cambridge) Interprocedural Shape Analysis with Separated Heap Abstractions Abstract: We describe an interprocedural shape analysis that makes use of spatial locality (i.e. the fact that most procedures modify only a small subset of the heap) in its representation of abstract states. Abstract states in our analysis are represented by formulae in separation logic's assertion language. As a result, computing the effect of procedure calls and returns on an abstract state is easy because the representation exhibits spatial locality mirroring the locality that is present in the concrete semantics. The benefits of this approach include improved speed, support for programs that deallocate memory, the handling of bounded numbers of heap cutpoints, and support for cyclic and shared data structures. This is joint work with Josh Berdine and Byron Cook. ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************