Papers

Peer-reviewed
2006

Reasoning about data-parallel pointer programs in a modal extension of separation logic

ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS
  • Susumu Nishimura

Volume
4019
Number
First page
293
Last page
307
Language
English
Publishing type
Research paper (scientific journal)
Publisher
SPRINGER-VERLAG BERLIN

This paper proposes a modal extension of Separation Logic [1, 2] for reasoning about data-parallel programs that manipulate heap allocated linked data structures. Separation Logic provides a formal means for expressing allocation of disjoint substructures, which are to be processed in parallel. A modal operator is also introduced to relate the global property of a parallel operation with the local property of each sequential execution running in parallel. The effectiveness of the logic is demonstrated through a formal reasoning on the parallel list scan algorithm featuring the pointer jumping technique.

Link information
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000239425400023&DestApp=WOS_CPL
ID information
  • ISSN : 0302-9743
  • Web of Science ID : WOS:000239425400023

Export
BibTeX RIS