Survey of research on program verification via separation logic

DOI10.13328/J.CNKI.JOS.005272zbMATH Open1399.68031MaRDI QIDQ4640971FDOQ4640971

Authors: Shengchao Qin, Zhiwu Xu, Zhong Ming 

Publication date: 25 May 2018

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

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)

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
• Title not available (Why is that?)

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)