Safe Modification of Pointer Programs in Refinement Calculus

DOI10.1007/978-3-540-70594-9_16MaRDI QIDQ3521993zbMATH OpenOpenAlexFDO

Authors Susumu Nishimura

Publication date 28 August 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70594-9_16

Mathematics Subject Classification ID

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

Recommendations

• A calculus of refinements for program derivations
• Pointer logic for verification of pointer programs
• Programming Languages and Systems
• scientific article; zbMATH DE number 1612488
• Frame rule for mutually recursive procedures manipulating pointers

Cites work

• A calculus of refinements for program derivations
• An algebraic treatment of procedure refinement to support mechanical verification
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Refinement Calculus
• Separation and information hiding

Cited in

(5)

• Stepwise refinement of heap-manipulating code in Chalice
• Automatically proving termination and memory safety for programs with pointer arithmetic
• scientific article; zbMATH DE number 2084334 (Why is no real title available?)
• Programming Languages and Systems
• Languages and Compilers for Parallel Computing

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Safe Modification of Pointer Programs in Refinement Calculus

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