Towards Modular Algebraic Specifications for Pointer Programs: A Case Study

DOI10.1007/978-3-540-73147-4_12MaRDI QIDQ3608820zbMATHOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(1)

• Modular specification of frame properties in JML

Describes a project that uses

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)