Extending separation logic with fixpoints and postponed substitution

DOI10.1016/J.TCS.2005.09.071zbMATH Open1086.68032OpenAlexW1974321100MaRDI QIDQ820139FDOQ820139

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

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

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)

Cites Work

• BI as an assertion language for mutable data structures
• Notions of computation and monads
• An axiomatic basis for computer programming
• Programming as a Discipline of Mathematical Nature
• Title not available (Why is that?)
• Systematic design of program transformation frameworks by abstract interpretation
• Title not available (Why is that?)
• Programming Languages and Systems
• Title not available (Why is that?)
• Algebraic Methodology and Software Technology
• 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)