Stepwise refinement of heap-manipulating code in Chalice

DOI10.1007/S00165-012-0254-3MaRDI QIDQ1941869zbMATH OpenOpenAlexFDO

Authors Kuat Yessenov, K. Rustan M. Leino

Publication date 22 March 2013

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/1721.1/105892

zbMATH Keywords

program verificationstepwise refinementdata refinementabstract predicatesChalicefractional permissionsheap refinement

Mathematics Subject Classification ID

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

Recommendations

• A calculus of refinements for program derivations
• A refinement methodology for object-oriented programs
• Safe Modification of Pointer Programs in Refinement Calculus
• Refinement for structured concurrent programs
• A program refinement tool

Cites work

• scientific article; zbMATH DE number 4050933 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• A constructive approach to the problem of program correctness
• A theoretical basis for stepwise refinement and the programming calculus
• Behavioral interface specification languages
• Blaming the client: on data refinement in the presence of pointers
• Certification of programs for secure information flow
• Class refinement as semantics of correct object substitutability
• Compositional noninterference from first principles
• Dafny: an automatic program verifier for functional correctness
• Modeling in Event B. System and software engineering.
• Program development by stepwise refinement
• Proof of correctness of data representations
• Separation logic and abstraction
• The B-Book

Cited in

(4)

• Verifying Whiley programs with Boogie
• A refinement methodology for object-oriented programs
• The formalism underlying EASYMAP: A precompiler for refinement-based exploration of hierarchical data organizations
• Data refinement of invariant based programs

Describes a project that uses

Uses Software

• Z
• Boogie
• VeriFast
• Chalice
• VCC
• ProB
• Rodin
• z3
• Spec#
• ACSL
• Eiffel
• Dafny

This page was built for publication: Stepwise refinement of heap-manipulating code in Chalice

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