Extending separation logic with fixpoints and postponed substitution

DOI10.1016/j.tcs.2005.09.071zbMath1086.68032OpenAlexW1974321100MaRDI QIDQ820139

É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)

Related Items (4)

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

Cites Work

• Notions of computation and monads
• Programming as a Discipline of Mathematical Nature
• BI as an assertion language for mutable data structures
• Systematic design of program transformation frameworks by abstract interpretation
• Algebraic Methodology and Software Technology
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item

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