Survey of research on program verification via separation logic

DOI10.13328/J.CNKI.JOS.005272MaRDI QIDQ4640971zbMATH OpenFDO

Authors Shengchao Qin, Zhiwu Xu, Zhong Ming

Publication date 25 May 2018

Full work available at URL https://doi.org/10.13328/J.CNKI.JOS.005272

zbMATH Keywords

functional correctnessmemory safetyprogram analysisprogram verificationseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Program Verification with Separation Logic
• Computer Science Logic
• Separation logic modulo theories
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Automated Verification of Shape and Size Properties Via Separation Logic

Cited in

(5)

• Reasoning about heap manipulating programs using automata techniques
• A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness
• scientific article; zbMATH DE number 5499339 (Why is no real title available?)
• Program Verification with Separation Logic
• Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday

This page was built for publication: Survey of research on program verification via separation logic

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