Synthesizing invariants by solving solvable loops

Article, Conference object English OPEN
Oliveira , S. ,; BENSALEM , S.; Prevosto , V.;
(2017)
  • Publisher: HAL CCSD
  • Related identifiers: doi: 10.5281/zenodo.893066, doi: 10.5281/zenodo.893067, doi: 10.1007/978-3-319-68167-2_22
  • Subject: Proof obligations | Linear transformations | [INFO]Computer Science [cs] | Polynomial optimization problem | Mathematical transformations | polynomial mapping | Loop invariants | invariant generation | Automation | Formal program verification | Optimization | [ INFO ] Computer Science [cs] | Automatic Generation | Open source tools | linearization

Conference of 15th International Conference on Automated Technology for Verification and Analysis, ATVA 2017 ; Conference Date: 3 October 2017 Through 6 October 2017; Conference Code:199839; International audience; Formal program verification faces two problems. The fir... View more
Share - Bookmark