Frama-C, a framework for the analysis and verification of C programs, with its WP plugin, provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to scale on deductive verification of complex programs. CoMeMoV, lead by Frédéric Loulergue, is a joint project of Université d’Orléans (LIFO, LMV Team), CEA List and Thales Research & Technology.