Back to Search
Start Over
Extending separation logic with fixpoints and postponed substitution
- Source :
-
Theoretical Computer Science . Feb2006, Vol. 351 Issue 2, p258-275. 18p. - Publication Year :
- 2006
-
Abstract
- 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 , 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. [Copyright &y& Elsevier]
- Subjects :
- *DATA structures
*LOGIC
*SEMANTICS
*AXIOMS
Subjects
Details
- Language :
- English
- ISSN :
- 03043975
- Volume :
- 351
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- 19592081
- Full Text :
- https://doi.org/10.1016/j.tcs.2005.09.071