********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * Ecole normale superieure * * ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Jeudi 9 Juin 2011, Salle R, 14h00-15h00 ************************* Typing and Static Analysis of Multi-Staged Programs Kwangkeun Yi (Seoul National University) Re'sume'/ Abstract: I will present a typing system and a general static analysis framework of multi-staged programs. Multi-staged programming have program text as first-class values (e.g. in runtime program generation in web/mobile apps, partial evaluation, and macro systems). Statically analyzing the semantics of multi-staged programs is challenging because the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. Our proposed static analysis framework consists of three steps: we first apply a semantics-preserving unstaging translation, then we apply conventional static anlaysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice: open code as values, unrestricted operations on references and intentional variable-capturing substitutions. We showed the correctness of the unstaging translation and a correctness condition of the three-step detouring of multi-staged static analysis. This work was co-work with Wontae Choi, Iksoon Kim, Baris Aktemur, Makoto Tatsuda, and Cristiano Calcagno. *** Vendredi 10 Juin 2011, Salle R, 14h00-15h00 ************************* DPLL is Abstract Interpretation Leopold Haller (Oxford University) Re'sume'/ Abstract: The DPLL algorithm for deciding propositional satisfiability is a fundamental algorithm with applications in several, diverse areas of computer science. In its modern formulation, it combines intelligent model search, deduction, and lemma generation in an elegant and highly efficient manner. An important question is whether the DPLL algorithm can be generalised to richer classes of problems. In this talk, I will outline how DPLL can naturally be viewed as an instance of abstract interpretation. The resulting abstract DPLL framework is a strict generalisation of DPLL to significantly richer logics and to non-Boolean domains. The instantiation of this framework with safety properties and abstract domains yields a powerful class of program analysis techniques which perform dynamic, property-driven domain-refinement. These results have immediate consequences for building program analysis tools. I will present an instantiation of the abstract DPLL framework in the domain of floating point intervals. This instantiation dynamically constructs a trace-partitioning over the base domain that is precise enough to prove complex programs correct, yet coarse enough to enable efficient analysis. *** Vendredi 17 Juin 2011, 14h00-15h00 ************************* *** Salle/Room: les hauts du DI' (Staircase A/Staircase of the Direction, 3rd floor). See: http://www.di.ens.fr/AccesDI.html ************************* Deriving temporal preorders using algebraic logic and abstraction Vijay D'Silva (Oxford University) Re'sume'/ Abstract: Temporal logics are formal languages for specifying properties of dynamic systems. A number of mathematical tools alleviate reasoning with such logics. These include preorders, fixed point characterisations, characteristic formulae, property preserving abstractions and optimal abstractions. These notions are studied separately and derived anew for every temporal logic. We show that these notions can be derived in a calculational manner from the grammar of a logic. The instantiation for specific logics (such as CTL, LTL, ACTL, etc) are derived by abstract interpretation of syntax. Our results are obtained using the algebraic semantics of Cousot and Cousot's Temporal Abstract Interpretation. Representation theorems from algebraic logic are then applied to translate these results into their conventional form and show when no conventional counterpart exists. *** Vendredi 24 Juin 2011, ***************************************** *** Horaire inhabituel: 10h30-11h30 *** Salle ihabituelle: les hauts du DI' (Staircase A of the Direction, 3rd floor). See: http://www.di.ens.fr/AccesDI.html ************************* Practical program verification for the working programmer with CodeContracts and Abstract Interpretation Francesco Logozzo (MSR Redmond) Re'sume'/ Abstract: In the talk I will describe Clousot, an abstract interpretation-based static analyzer used as verifier for the CodeContracts. Clousot is routinely used every day by many .NET programmers. In the first part of the talk I will recall what contracts are (essentially preconditions, postconditions and object invariants), why they are almost universally accepted as good software engineering practice. Nevertheless, their adoption is very low in practice, mainly for two reasons: (i) they require a non-negligible change in the build environment which very few professional programmers are willing to pay (e.g. a new language or a new or non-standard compiler or poor IDE integration ...); (ii) the static verification tools are either absent or they require far too much help and hugely miss automation. The CodeContracts API is an answer to (i). Clousot is an answer to (ii). In the second part of the talk, I will dig deeper into the Clousot architecture, explaining: (i) why unlikely similar tools we decided to base it on abstract interpretation (essentially because of automation, inference power, generality, fine control of the cost/tradeoff ratio ...); and (ii) the new abstract domains (numerical, universal, existential, etc.) we designed and implemented. The CodeContracts API is part of .NET 4.0. Clousot can be downloaded from the DevLabs: http://msdn.microsoft.com/es-AR/devlabs/dd491992.aspx Joint work with Manuel Fahndrich and Mike Barnett. *** Vendredi 24 Juin 2011, 14h00 ************************* *** Lieu/Localization: Ecole Normale Supérieure, Room E314, Entrance at the 24, Lhomond Street, see map http://www.di.ens.fr/~rival/hdr/plan-en.jpg ************************* Habilitation à Diriger des Recherches Domaines abstraits pour l'analyse statique de programmes manipulant des structures de données complexes // Abstract domains for the static analysis of programs manipulating complex data-structures Xavier Rival (INRIA & ENS) Re'sume': Au cours de cette soutenance, nous présenterons un domaine abstrait paramètrique pour l'analyse statique par interprétation abstraite de programmes manipulant des structures de données complexes, allouées dynamiquement, et poserons ainsi les fondations pour une famille d'analyses statiques ayant pour but de calculer une sur-approximation des états accessibles de tels programmes. Notre domaine peut être paramétré non seulement par un ensemble de définitions inductives de structures de données mais aussi par le choix d'un domaine numérique sous-jacent. Les valeurs abstraites peuvent être vues soit comme des graphes, soit comme des formules dans un sous-ensemble de la logique de séparation avec définitions inductives. Nous décrirons l'abstraction induite par ce domaine ainsi que les principales fonctions d'analyse. En particulier, nous considérerons un opérateur de dépliage qui permet de raffiner localement la description d'un ensemble d'états et ainsi de calculer avec précision des post-conditions. Ensuite, nous nous intéresserons à une famille d'opérateurs d'union et d'élargissement, afin de garantir la terminaison de l'analyse. Dans la suite de notre exposé, nous considérerons plusieurs applications de cette analyse statique. Nous montrerons comment celle-ci peut être adaptée afin traiter de manière précise des programmes écrits dans un langage autorisant des opérations bas-niveau, tel que C. Ensuite, nous nous intéresserons à l'analyse de programmes avec des fonctions récursives, et introduirons un opérateur d'élargissement capable de calculer des définitions inductives adaptées à l'abstraction conjoint de la pile d'appel et de la mémoire d'un programme donné. Enfin, la dernière partie de cet exposé sera consacrée aux perspectives d'extensions de notre analyse, plus particulièrement pour une prise en compte plus systématique de la notion de partage dans les structures de données, pour la généralisation de l'inférence de définitions inductives et pour la mise au point d'un opérateur de réduction. Nous discuterons également les problèmes posés par l'implantation d'un domaine abstrait pour structures de données complexes sous la forme d'une librairie séparée, comme cela a pu être fait pour les domaines abstraits numériques. // Abstract: In this defense, we will present a parametric abstract domain for the static analysis by abstract interpretation of programs which manipulate complex and dynamically allocated data-structures. We will set up the foundations for a family of static analyses to compute an over-approximation of the reachable states of programs using such structures. Our domain can be parameterized with a set of inductive definitions capturing a set of relevant data-structures and by the choice of an underlying numerical domain. Abstract values can be viewed either as graphs, or as formulas in a subset of separation logic extended with inductive definitions. We will describe the abstraction induced by this domain, and the main static analysis operators. In particular, we will consider the unfolding operator, which allows to refine in a local manner an abstract value, so as to allow precise algorithms for the computation of post-conditions. Then, we will discuss a set of join and widening operators, so as to guarantee the termination of our static analyses. In the second part of the talk, we will consider several applications of our static analysis. We will show how it can be adapted in order to treat in a precise way specific features of programs written in languages which allow low level memory operations, such as the C language. Then, we will focus on the analysis of programs with recursive procedures and we will introduce a powerful widening operator, which is able to infer accurate inductive definitions to be used to summarize the call-stack of a specific program together with the memory. Finally, the last part of this talk will be devoted to perspectives for extensions of our analysis. We will mainly focus on a better treatment of the notion of sharing in data-structures with the help of a dedicated abstract domain, on the generalization of the scheme for inferring inductive definitions, and on the design of a reduction operator. We will also discuss the issues raised by the implementation of abstract domains for the static analysis of programs manipulating complex data-structures as standalone libraries, as achieved for numerical abstract domains. ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************