@inproceedings{591601e96026488087e03e7252a9eb94,
title = "Synthesizing invariants by solving solvable loops",
abstract = "Formal program verification faces two problems. The first problem is related to the necessity of having automated solvers that are powerful enough to decide whether a formula holds for a set of proof obligations as large as possible, whereas the second manifests in the need of finding sufficiently strong invariants to obtain correct proof obligations. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented on top of the open-source tool Pilat.",
author = "\{de Oliveira\}, Steven and Saddek Bensalem and Virgile Prevosto",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017 ; Conference date: 03-10-2017 Through 06-10-2017",
year = "2017",
month = jan,
day = "1",
doi = "10.1007/978-3-319-68167-2\_22",
language = "English",
isbn = "9783319681665",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "327--343",
editor = "Deepak D{\textquoteright}Souza and \{Narayan Kumar \}, K.",
booktitle = "Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Proceedings",
}