Putting the squeeze on array programs: loop verification via inductive rank reduction

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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