Compositional recurrence analysis

Azadeh Farzan, Zachary Kincaid

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

17 Scopus citations

Abstract

This paper presents a new method for automatically generating numerical invariants for imperative programs. The procedure computes a transition formula which overapproximates the behaviour of a given input program. It is compositional in the sense that it operates by decomposing the program into parts, computing a transition formula for each part, and then composing them. Transition formulas for loops are computed by extracting recurrence relations from a transition formula for the loop body and then computing their closed forms. Experimentation demonstrates that this method is competitive with leading verification techniques based on abstraction refinement.

Original languageEnglish (US)
Title of host publicationProceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages57-64
Number of pages8
ISBN (Electronic)9780983567851
DOIs
StatePublished - Aug 11 2016
Externally publishedYes
Event15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 - Austin, United States
Duration: Sep 27 2015Sep 30 2015

Other

Other15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
CountryUnited States
CityAustin
Period9/27/159/30/15

All Science Journal Classification (ASJC) codes

  • Engineering (miscellaneous)
  • Computer Science Applications
  • Software

Cite this

Farzan, A., & Kincaid, Z. (2016). Compositional recurrence analysis. In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 (pp. 57-64). [7542253] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/FMCAD.2015.7542253