friends of invader


SpaceInvader, a descendant of Smallfoot, is a cousin of SLAyer. SpaceInvader acknowledges the excellent work done in the context of TVLA.

Some of the theoretical work underpinning SpaceInvader was done jointly with Josh Berdine, Byron Cook, Oukseh Lee and Thomas Wies.

Some recent tools related to SpaceInvader and Smallfoot include jStar, Vericool, Verifast, Chalice, Hip, Heap Hop, Xisa, Thor and SmallfootRG .

Although Invader is not being actively maintained, there are other tools which contain many of its ideas.

SLAyer, which initially co-evolved with Invader, continues development  at Microsoft Research.

Predator, a successor to Invader, implements many of the same ideas, and is also being actively maintained. It is available as a gcc plugin. 

An extension of Invader to deal with multiple views (overlaid data structures) provides perhaps a better starting point for building on the Invader codebase than the original. (Note, though, that this more recent version cannot be used to verify the device driver examples from the CAV’08 paper.)

The Spaceinvader Blog.