Finding Model-Checkable Needles in Large Source Code Haystacks: Modular Bug-Finding via Static Analysis and Dynamic Invariant Discovery. - Mohammad Amin Alipour; Alex Groce; Chaoqiang Zhang; Anahita Sanadaji; Gokul Caushik (CoRR, 2016)