TY - GEN
T1 - Compositional recurrence analysis revisited
AU - Kincaid, Zachary
AU - Breck, Jason
AU - Boroujeni, Ashkan Forouhi
AU - Reps, Thomas
N1 - Publisher Copyright:
© 2017 ACM.
PY - 2017/6/14
Y1 - 2017/6/14
N2 - Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural version of CRA that handles recursive procedures. The problem is non-trivial because there is an "impedance mismatch" between CRA, which relies on analysis techniques based on regular languages (i.e., Tarjan's path-expression method), and the context-free-language underpinnings of contextsensitive analysis. We show how to address this impedance mismatch by augmenting the CRA abstract domain with additional operations. We call the resulting algorithm Interprocedural CRA (ICRA). Our experiments with ICRA show that it has broad overall strength compared with several state-of-the-art software model checkers.
AB - Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural version of CRA that handles recursive procedures. The problem is non-trivial because there is an "impedance mismatch" between CRA, which relies on analysis techniques based on regular languages (i.e., Tarjan's path-expression method), and the context-free-language underpinnings of contextsensitive analysis. We show how to address this impedance mismatch by augmenting the CRA abstract domain with additional operations. We call the resulting algorithm Interprocedural CRA (ICRA). Our experiments with ICRA show that it has broad overall strength compared with several state-of-the-art software model checkers.
KW - Invariant generation
KW - Resource bounds
UR - http://www.scopus.com/inward/record.url?scp=85025146971&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85025146971&partnerID=8YFLogxK
U2 - 10.1145/3062341.3062373
DO - 10.1145/3062341.3062373
M3 - Conference contribution
AN - SCOPUS:85025146971
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 248
EP - 262
BT - PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Cohen, Albert
A2 - Vechev, Martin
PB - Association for Computing Machinery
T2 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
Y2 - 18 June 2017 through 23 June 2017
ER -