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 2 mai, 10h30

                                --------------
                                Timothy Bourke
                                --------------

                                 Inria Paris

                  ==========================================
                  Towards the verified compilation of Lustre
                  ==========================================

Synchronous dataflow languages allow engineers to design and verify
systems at the level of block diagrams that are automatically compiled
into executable code. The most striking example is the SCADE Suite
tool of ANSYS/Esterel Technologies which is DO-178B/C qualified for
the aerospace and defense industries.

Formal modelling and verification in an interactive theorem prover can
potentially complement the industrial certification of such tools to
give precise definitions of language features and increased confidence
in their correct compilation.

In this talk, I will summarise early work led by Marc Pouzet on
formally modelling the core features of a Lustre-like language and
verifying several of its source-to-source compilation passes in the
Coq proof assistant. I will then present recent developments on
verifying the pass that transforms dataflow equations, where programs
manipulate streams of values, into imperative code, where programs
iteratively perform stateful computations. Finally, I will describe
the obstacles and work that remain.

This talk describes joint work with Pierre-Évariste Dagand,
Marc Pouzet, and Lionel Rieg.