Article ID Journal Published Year Pages File Type
436773 Theoretical Computer Science 2006 18 Pages PDF
Abstract

We are interested in separation-logic-based static analysis of programs that use shared mutable data structures. In this paper, we introduce backward and forward analysis for a separation logic called BIμν, an extension of separation logic [Ishtiaq and O’Hearn, BI as an assertion language for mutable data structures, in: POPL’01, 2001, pp. 14–26], to which we add fixpoint connectives and postponed substitution. This allows us to express recursive definitions within the logic as well as the axiomatic semantics of while statements.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics