An Assume Guarantee Approach for Checking Quantified Array Assertions

DOI10.1007/978-3-642-17796-5_15zbMath1308.68047OpenAlexW2127524911MaRDI QIDQ3067480

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)

Uses Software

• ACSAR
• SLAM
• PVS

Cites Work

• Unnamed Item
• Lifting abstract interpreters to quantified logical domains
• Abstraction Refinement for Quantified Array Assertions
• Lazy abstraction
• Invariant Synthesis for Combined Theories
• An axiomatic basis for computer programming
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: An Assume Guarantee Approach for Checking Quantified Array Assertions