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)