Space Invading Systems Code

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.

Authors

• Cristiano Calcagno
• Dino Distefano
• Peter W. O'Hearn
• Hongseok Yang

Keywords

No keywords are indexed for this paper.