SpaceInvader 1.1 is a prototype analyzer for C programs, based on separation logic.

Download the distribution. (BSD source license)

Abduction Prover Sources. (BSD source license)

Invader was developed in the period 2005-2008. It is no longer being actively maintained. See SLAyer and Predator and other links in the Friends section for current tools related to it.