Verifying Array Programs by Transforming Verification Conditions

DOI10.1007/978-3-642-54013-4_11MaRDI QIDQ2938066zbMATH OpenOpenAlexFDO

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

Publication date 13 January 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-54013-4_11

Mathematics Subject Classification ID

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

Recommendations

• Artificial Intelligence and Symbolic Computation
• A rule-based verification strategy for array manipulating programs
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• scientific article; zbMATH DE number 4049004
• Verifying array manipulating programs with full-program induction
• Transformational Verification of Parameterized Protocols Using Array Formulas
• Program verification using constraint handling rules and array constraint generalizations
• Automatic Verification of Integer Array Programs
• Verifying array manipulating programs by tiling
• Scaling bounded model checking by transforming programs with arrays

Cited in

(19)

• Program verification using constraint handling rules and array constraint generalizations
• scientific article; zbMATH DE number 7447758 (Why is no real title available?)
• Property checking array programs using loop shrinking
• Automatic Verification of Integer Array Programs
• Verification of imperative programs by constraint logic program transformation
• Scaling bounded model checking by transforming programs with arrays
• Copy complexity of Horn formulas with respect to unit read-once resolution
• Cell morphing: from array programs to array-free Horn clauses
• Verifying array manipulating programs by tiling
• Verification problem for linear programs with Boolean arrays
• Loop verification with invariants and contracts
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• An assume guarantee approach for checking quantified array assertions
• Polycheck: dynamic verification of iteration space transformations on affine programs
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• Analyzing Array Manipulating Programs by Program Transformation
• scientific article; zbMATH DE number 1738288 (Why is no real title available?)
• scientific article; zbMATH DE number 6687732 (Why is no real title available?)
• A rule-based verification strategy for array manipulating programs

Describes a project that uses

Uses Software

• FunArray
• HSF
• z3

This page was built for publication: Verifying Array Programs by Transforming Verification Conditions

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