Compositional recurrence analysis revisited

Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas Reps

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationPLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlbert Cohen, Martin Vechev
PublisherAssociation for Computing Machinery
Pages248-262
Number of pages15
ISBN (Electronic)9781450349888
DOIs
StatePublished - Jun 14 2017
Event38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
Duration: Jun 18 2017Jun 23 2017

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
VolumePart F128414

Other

Other38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
CountrySpain
CityBarcelona
Period6/18/176/23/17

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Invariant generation
  • Resource bounds

Fingerprint Dive into the research topics of 'Compositional recurrence analysis revisited'. Together they form a unique fingerprint.

  • Cite this

    Kincaid, Z., Breck, J., Boroujeni, A. F., & Reps, T. (2017). Compositional recurrence analysis revisited. In A. Cohen, & M. Vechev (Eds.), PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 248-262). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Vol. Part F128414). Association for Computing Machinery. https://doi.org/10.1145/3062341.3062373