Short works
  -  Playing with abstraction and refinement for managing  features interactions. 2000. (In ZB 2000 )
  
-  Incremental Proof of the Producer/Consumer Property for the PCI Protocol. 2002. (In ZB 2002 )
  
-  Formal derivation of spanning tree algorithms. 2003. (In ZB 2003 )
  
-  Refinement and reachability in Event B. 2005. (In ZB 2005 )