Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic

DOI10.1134/S0361768822080023MaRDI QIDQ6486105zbMATH OpenFDO

Authors M. U. Mandrykin

Publication date 5 January 2023

Published in Programming and Computer Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/S0361768822080023

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Proving termination and memory safety for programs with pointer arithmetic
• Automated Deduction – CADE-20
• Automatically proving termination and memory safety for programs with pointer arithmetic
• A decision procedure for separation logic in SMT
• Computer Science Logic

This page was built for publication: Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic

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