@misc{indiciaea0508b6f61f1, title = {Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses}, author = {Emanuele De Angelis and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti}, year = {2015}, doi = {10.1017/s1471068415000289}, url = {https://arxiv.org/abs/1507.05877}, note = {Source identifier: 1507.05877} }