@inproceedings{4bf72e83e8b84476b582b5f8c2000bdc,
title = "Compositional recurrence analysis",
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.",
author = "Azadeh Farzan and Zachary Kincaid",
note = "Publisher Copyright: {\textcopyright} 2015 FMCAD Inc.; 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 ; Conference date: 27-09-2015 Through 30-09-2015",
year = "2016",
month = aug,
day = "11",
doi = "10.1109/FMCAD.2015.7542253",
language = "English (US)",
series = "Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "57--64",
editor = "Roope Kaivola and Thomas Wahl",
booktitle = "Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015",
address = "United States",
}