Our paper "FunFrog: Bounded Model Checking with Interpolation-based Function Summarization" has been accepted to ATVA 2012