Abstract: The literature records various formal and automatic techniques allowing to ensure that a system never violate some given requirements ans in particular some security policies. Mainly, we distinguish two groups of approaches: static analysis and dynamic analysis. Static analysis aims to verify software before running them while dynamic analysis techniques check them during their executions. Generally, both of these techniques are needed since they complement each other: There are some properties that could not be verified dynamically and vice-versa. For instance, liveness properties (something good will happen) could not be ensured dynamically. Other properties that depend on some values known only at execution time could not be verified statically. However, static analysis are in most all cases preferable when the problem can be resolved before the execution.
Recently, many researchers have been interested by rewriting techniques in order to gather advantages of both static and dynamic methods. The idea consists in modifying statically a software, so that the new version respects the requested requirements. The rewritten software is generated from the original one by adding, when necessary, some tests at some critical points so that it behaves like requested.

Brief Biography of the Speaker:
He received a Ph.D. in Computer Science with General Honors, Computer Science Department, Laval University, Canada.
Currently he is a Full Professor in Computer Science. Computer Science Department, Laval University, Quebec, Canada, he works on computer Security, and contributed in many project worldwide.
He received CIPA Awards/Canadian Information Productivity Awards/2001: MaliCots project (LSFM research group). CIPA'2001. He received Star Professor/Laval University, Canada 2002/ 2003/ 2005/ 2006/ 2008: For the excellent quality of teaching. He was a visiting professor at Fujita's Laboratory Iwate Prefectural University, Iwate, Japan on 2008, for six months doing a joint work with Prof. Hamido Fujita, He got a joint patent on software methodology.