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 - Rocquencourt
                         Amphi Turing du bâtiment 1

                            Lundi 4 janvier, 10h30

                              -----------------
                              Jean-Marie Madiot
                              -----------------

                             Princeton University

                 ============================================
                 Verified reasoning for concurrent C programs
                 ============================================

The software toolchain includes static analyzers to check assertions
about your program; optimizing compilers to translate your program to
machine language; operating systems and libraries to supply context
for your program. The Verified Software Toolchain project assures with
machine-checked proofs that the assertions claimed for C programs at
the top of the toolchain really hold in the machine-language program,
running in the operating-system context.

To this framework, we add program logic rules for concurrent
primitives in the style of concurrent separation logic (CSL), e.g. for
the acquiring and releasing of locks. The rules are expressed in a
richly decorated memory model, that we erase down to CompCert's, and,
eventually, down to weaker memory models. Finally, we add to the
decoration a notion of ghost state, to recover the loss of logical
expressiveness induced by the sole use of CSL's resource invariants.