Stepwise refinement of heap-manipulating code in Chalice
From MaRDI portal
Publication:1941869
DOI10.1007/s00165-012-0254-3zbMath1259.68034MaRDI QIDQ1941869
K. Rustan M. Leino, Kuat Yessenov
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
stepwise refinement; data refinement; program verification; abstract predicates; Chalice; fractional permissions; heap refinement
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Uses Software