Eliminating stack overflow by abstract interpretation

An important correctness criterion for software running on embedded microcontrollers is stack safety : a guarantee that the call stack does not overflow. Our first contribution is a method for statically guaranteeing stack safety of interrupt-driven embedded software using an approach based on context-sensitive dataflow analysis of object code. We have implemented a prototype stack analysis tool that targets software for Atmel AVR...