Putting the squeeze on array programs: loop verification via inductive rank reduction
From MaRDI portal
Publication:784119
DOI10.1007/978-3-030-39322-9_6OpenAlexW2998875295MaRDI QIDQ784119
Shachar Itzhaky, Sharon Shoham, Noam Rinetzky, Oren Ish-Shalom
Publication date: 5 August 2020
Full work available at URL: https://arxiv.org/abs/2106.00937
Related Items
\textsc{Diffy}: inductive reasoning of array programs using difference invariants, Data abstraction: a general framework to handle program verification of data structures, Interpolation and amalgamation for arrays with MaxDiff, Run-time complexity bounds using squeezers