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

zbMATH Keywords

program verificationseparation logicprogram analysismemory safetyfunctional correctness

Mathematics Subject Classification ID

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) Logic in computer science (03B70)

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
• Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday
• Program Verification with Separation Logic
• 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?)

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)