論文

査読有り
2006年

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

ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS
  • Susumu Nishimura

4019
開始ページ
293
終了ページ
307
記述言語
英語
掲載種別
研究論文(学術雑誌)
出版者・発行元
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.


リンク情報
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情報
  • ISSN : 0302-9743
  • Web of Science ID : WOS:000239425400023

エクスポート
BibTeX RIS