An assume guarantee approach for checking quantified array assertions

DOI10.1007/978-3-642-17796-5_15MaRDI QIDQ3067480zbMATH OpenOpenAlexFDO

Authors Mohamed Nassim Seghir

Publication date 21 January 2011

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-17796-5_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Abstraction Refinement for Quantified Array Assertions
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Verifying Array Programs by Transforming Verification Conditions
• Analyzing Array Manipulating Programs by Program Transformation
• Quantifiers on demand

Cites work

• Abstraction Refinement for Quantified Array Assertions
• An axiomatic basis for computer programming
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• Invariant Synthesis for Combined Theories
• Lazy abstraction
• Lifting abstract interpreters to quantified logical domains
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Abstraction Refinement for Quantified Array Assertions
• Integrated Formal Methods
• Quantifiers on demand

Describes a project that uses

Uses Software

• ACSAR
• SLAM
• PVS

This page was built for publication: An assume guarantee approach for checking quantified array assertions

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