ABSTRACT. In this paper, we propose Android Stack Systems (ASS), a formal model to capture key mechanisms of Android multi-tasking such as activities, the back stack, launch modes, as well as task affinities. The model is based on pushdown systems with multiple stacks, and focuses on the evolution of the back stack of the Android system when interacting with activities carrying specific launch modes and task affinities. For formal analysis, we study the reachability problem of ASS. While the general problem is shown to be undecidable, we identify expressive fragments for which various verification techniques for pushdown systems or their decidable extensions are harnessed to show that the reachability problem is decidable.