FreeSafeTy (Free is made Safe by Types) is a type-based memory usage verifier for C programs. FreeSafeTy can verify the following properties on memory usage. Lack of memory leak. Lack of double free. Lack of read/write to deallocated memory cell. For technical issues on the verifier, see our papers. Download FreeSafeTy 0.2 (.tar.gz) Install You need GLPK, ocaml-glpk and OMake to install FreeSafeTy