Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 30 mai, 10h30 ------------ Martin Bodin ------------ Inria Rennes =================================================== Pushing the Frame Rule into Abstract Interpretation =================================================== Abstract interpretation is a very powerful tool to analyse programs. In a nutshell, it consists of providing an abstract state of for each step of a given program's execution, and proving that each of these abstract states yield the next one in the control flow. This framework allows to locally analyse programs using a variety of powerful techniques, such as widening. We are aiming at analysing JavaScript programs and prove the analysis correct in Coq. This significantly increases the difficulty of the task and forces us to do it in a modular way. There have already been some work on a separation logic for JavaScript. Separation logic provides the frame rule, which eases the definition of modular analyses. However, the frame rules does not easily mix with abstract interpretation. We present a domain of heaps of interlinked extensible records based on both separation logic and abstract interpretation. The domain features spatial conjunction and uses summary nodes from shape analyses. We show how this domain can accommodate an abstract interpretation including a frame rule.