LOPSTR Conference 2008 Conference Paper
Space Invading Systems Code
- Cristiano Calcagno
- Dino Distefano
- Peter W. O'Hearn
- Hongseok Yang
Abstract Space Invader is a static analysis tool that aims to perform accurate, automatic verification of the way that programs use pointers. It uses separation logic assertions [10, 11] to describe states, and works by performing a proof search, using abstract interpretation to enable convergence. As well as having roots in separation logic, Invader draws on the fundamental work of Sagiv et. al. on shape analysis [12]. It is complementary to other tools - e. g. , SLAM [1], Blast [8], ASTRÉE [6] - that use abstract interpretation for verification, but that use coarse or limited models of the heap.