A rule-based verification strategy for array manipulating programs

DOI10.3233/FI-2015-1257MaRDI QIDQ3187012zbMATH OpenFDO

Authors Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

Publication date 15 August 2016

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/FI-2015-1257

Mathematics Subject Classification ID

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

Recommendations

• Verifying Array Programs by Transforming Verification Conditions
• Program verification using constraint handling rules and array constraint generalizations
• Verification of imperative programs by constraint logic program transformation
• Automatic Verification of Integer Array Programs
• Analyzing Array Manipulating Programs by Program Transformation

Cited in

(11)

• Cell morphing: from array programs to array-free Horn clauses
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Verifying Array Programs by Transforming Verification Conditions
• Bounded symbolic execution for runtime error detection of Erlang programs
• Automatic Verification of Integer Array Programs
• Program verification using constraint handling rules and array constraint generalizations
• Predicate pairing for program verification
• Verification of imperative programs by constraint logic program transformation
• Verifying array manipulating programs with full-program induction
• Verifying array manipulating programs by tiling
• Putting the squeeze on array programs: loop verification via inductive rank reduction

This page was built for publication: A rule-based verification strategy for array manipulating programs

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