Stepwise refinement of heap-manipulating code in Chalice

DOI10.1007/s00165-012-0254-3zbMath1259.68034OpenAlexW2056896376MaRDI QIDQ1941869

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

stepwise refinementdata refinementprogram verificationabstract predicatesChalicefractional permissionsheap refinement

Mathematics Subject Classification ID

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

Related Items (1)

Verifying Whiley programs with Boogie

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compositional noninterference from first principles
• A theoretical basis for stepwise refinement and the programming calculus
• Blaming the client: on data refinement in the presence of pointers
• Class refinement as semantics of correct object substitutability
• Proof of correctness of data representations
• Behavioral interface specification languages
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Basis for Verifying Multi-threaded Programs
• Certification of programs for secure information flow
• The B-Book
• Separation logic and abstraction
• A constructive approach to the problem of program correctness
• Program development by stepwise refinement

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