Formal Verification of Memory PropertiesWe are interested in the formal verification of low-level software. For this purpose, we have developed in the Coq proof assistant formalizations of Separation logic (as presented in the survey by John C. Reynolds). We have applied these formalizations to several use-cases, including: the verification of the heap manager of the Topsy operating system (paper) the verification of arithmetic function
