AVERILES : verification of C programs with dynamic memory
AVERISS : automatic software verification for programs with data manipulation, procedure calls, parameterization, concurrency
BINCOA : binary code analysis
PREDATOR : a tool for checking manipulation of dynamic data structures using separation logic
XISA : extensible inductive shape analysis
SpaceInvader : shape analysis using separation logic