Stepwise refinement of heap-manipulating code in Chalice
type: Item
instance of: scholarly article
title: Stepwise refinement of heap-manipulating code in Chalice
zbMATH Open document ID: 1259.68034
author: Kuat Yessenov
author: K. Rustan M. Leino
published in: Formal Aspects of Computing
publication date: 2013-03-22T00:00:00Z
full work available at URL: http://hdl.handle.net/1721.1/105892
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 6148336
zbMATH Keywords: stepwise refinement
zbMATH Keywords: data refinement
zbMATH Keywords: heap refinement
zbMATH Keywords: Chalice
zbMATH Keywords: abstract predicates
zbMATH Keywords: fractional permissions
zbMATH Keywords: program verification
describes a project that uses: ACSL
describes a project that uses: Rodin
describes a project that uses: ProB
describes a project that uses: VCC
describes a project that uses: VeriFast
describes a project that uses: Z
describes a project that uses: Dafny
describes a project that uses: Eiffel
describes a project that uses: z3
describes a project that uses: Chalice
describes a project that uses: Boogie
describes a project that uses: Spec#
MaRDI profile type: Publication
OpenAlex ID: W2056896376
cites work: The B-Book
cites work: Q3569584
cites work: Class refinement as semantics of correct object substitutability
cites work: Q4813391
cites work: Certification of programs for secure information flow
cites work: A constructive approach to the problem of program correctness
cites work: Q4144755
cites work: Blaming the client: on data refinement in the presence of pointers
cites work: Behavioral interface specification languages
cites work: Proof of correctness of data representations
cites work: Dafny: An Automatic Program Verifier for Functional Correctness
cites work: Q3787422
cites work: A Basis for Verifying Multi-threaded Programs
cites work: A theoretical basis for stepwise refinement and the programming calculus
cites work: Q3996918
cites work: Compositional noninterference from first principles
cites work: Separation logic and abstraction
cites work: Q4301167
cites work: Program development by stepwise refinement
DOI: 10.1007/S00165-012-0254-3
description: scientific article; zbMATH DE number 6148336