Simplifying the Verification of Quantified Array Assertions via Code Transformation

DOI10.1007/978-3-642-38197-3_13MaRDI QIDQ2848907zbMATH OpenOpenAlexFDO

Authors Mohamed Nassim Seghir, Martin Brain

Publication date 13 September 2013

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38197-3_13

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying Array Programs by Transforming Verification Conditions
• Abstraction Refinement for Quantified Array Assertions
• An assume guarantee approach for checking quantified array assertions
• Transformational Verification of Parameterized Protocols Using Array Formulas
• Artificial Intelligence and Symbolic Computation
• Scaling bounded model checking by transforming programs with arrays
• scientific article; zbMATH DE number 7453193
• A rule-based verification strategy for array manipulating programs
• Putting the squeeze on array programs: loop verification via inductive rank reduction

Cited in

(8)

• Verifying array manipulating programs with full-program induction
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Scaling bounded model checking by transforming programs with arrays
• Verifying Array Programs by Transforming Verification Conditions
• Abstraction Refinement for Quantified Array Assertions
• An assume guarantee approach for checking quantified array assertions
• Automatic program instrumentation for automatic verification
• scientific article; zbMATH DE number 6687732 (Why is no real title available?)

This page was built for publication: Simplifying the Verification of Quantified Array Assertions via Code Transformation

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