Compositional recurrence analysis revisited

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

Research output: Contribution to journalArticle

3 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 context-sensitive 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)
Pages (from-to)248-262
Number of pages15
JournalACM SIGPLAN Notices
Volume52
Issue number6
DOIs
StatePublished - Jun 14 2017

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Invariant generation
  • Resource bounds

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

  • Cite this