Towards Modular Algebraic Specifications for Pointer Programs: A Case Study

DOI10.1007/978-3-540-73147-4_12zbMATH Open1186.68116OpenAlexW2116518308MaRDI QIDQ3608820FDOQ3608820

Authors: Claude Marché 

Publication date: 6 March 2009

Published in: Rewriting, Computation and Proof (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73147-4_12

Recommendations

• Efficient modular SMT-based model checking of pointer programs
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Structuring and modularizing algebraic specifications: the PLUSS specification language, evolutions and perspectives
• Proving pointer programs in higher-order logic
• Proving pointer programs in higher-order logic.
• Towards pointer algebra
• Concise read-only specifications for better synthesis of programs with pointers
• Completeness and expressiveness of pointer program verification by separation logic
• Publication:4721633

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Cited In (1)

• Modular specification of frame properties in JML

Uses Software

• KRAKATOA
• SMT-LIB
• JML
• Caduceus

This page was built for publication: Towards Modular Algebraic Specifications for Pointer Programs: A Case Study

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