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

DOI10.1007/978-3-030-39322-9_6MaRDI QIDQ784119zbMATH OpenOpenAlexFDO

Authors Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham

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)

Recommendations

• Verifying array manipulating programs with full-program induction
• Artificial Intelligence and Symbolic Computation
• Verifying Array Programs by Transforming Verification Conditions
• scientific article; zbMATH DE number 4049004
• A rule-based verification strategy for array manipulating programs
• Scaling bounded model checking by transforming programs with arrays
• Program verification using constraint handling rules and array constraint generalizations

Cited in

(6)

• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Interpolation and amalgamation for arrays with MaxDiff
• Run-time complexity bounds using squeezers
• Data abstraction: a general framework to handle program verification of data structures
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• scientific article; zbMATH DE number 1738288 (Why is no real title available?)

This page was built for publication: Putting the squeeze on array programs: loop verification via inductive rank reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q784119)