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 15 avril, 10h30

                                --------------
                                Léon Gondelman
                                --------------

                              Radboud University

       ===============================================================
       Semi-Automated Reasoning About Non-Determinism in C Expressions
       ===============================================================

Research into C verification often ignores that the C standard leaves the 
evaluation order of expressions unspecified, and assigns undefined behavior to 
write-write or read-write conflicts in subexpressions—so called “sequence point 
violations”. Undefined behavior may cause a program to crash or to have 
arbitrary results, so it is essential to make sure that C programs are free of 
undefined behavior for any expression evaluation order.

Together with Dan Frumin and Robbert Krebbers, we have recently developed a 
concurrent separation logic with a verification condition generator for a semi-
automated reasoning about non-determinism in C expressions. The key novelty of 
our approach is a symbolic execution algorithm which is used to automatically 
determine how memory resources should be distributed among subexpressions.

In this talk I will explain our verification condition generator and symbolic 
executor, and how one can use them to reason about C programs within the Coq 
proof assistant.