Abstract
We present in this paper a new technique for generating polynomial invariants, divided in two independent parts: a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification.
Cite
CITATION STYLE
de Oliveira, S., Bensalem, S., & Prevosto, V. (2016). Polynomial invariants by linear algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9938 LNCS, pp. 479–494). Springer Verlag. https://doi.org/10.1007/978-3-319-46520-3_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
