Stepwise refinement of heap-manipulating code in Chalice

DOI10.1007/S00165-012-0254-3zbMATH Open1259.68034OpenAlexW2056896376MaRDI QIDQ1941869FDOQ1941869

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

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

zbMATH Keywords

program verificationstepwise refinementdata refinementabstract predicatesChalicefractional permissionsheap refinement

Mathematics Subject Classification ID

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

Cites Work

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

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

Uses Software

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

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)