Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
436773 | Theoretical Computer Science | 2006 | 18 Pages |
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