Extending separation logic with fixpoints and postponed substitution

DOI10.1016/J.TCS.2005.09.071MaRDI QIDQ820139zbMATH OpenOpenAlexFDO

Authors Élodie-Jane Sims

Publication date 6 April 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2005.09.071

zbMATH Keywords

abstract interpretationseparation logicfixpoint\(sp\)\(wlp\)

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Algebraic Methodology and Software Technology
• Relational Parametricity and Separation Logic
• Relational Parametricity and Separation Logic
• Separation Logic for Higher-Order Store
• Algebraic separation logic

Cites work

• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 2087567 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• An axiomatic basis for computer programming
• BI as an assertion language for mutable data structures
• Notions of computation and monads
• Programming Languages and Systems
• Programming as a Discipline of Mathematical Nature
• Systematic design of program transformation frameworks by abstract interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Extended transitive separation logic
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Algebraic Methodology and Software Technology
• Logics and Bisimulation Games for Concurrency, Causality and Conflict
• Transitive Separation Logic

This page was built for publication: Extending separation logic with fixpoints and postponed substitution

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