@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",

}