Sciweavers

Share
AMAST
2006
Springer

Reasoning About Data-Parallel Pointer Programs in a Modal Extension of Separation Logic

10 years 6 months ago
Reasoning About Data-Parallel Pointer Programs in a Modal Extension of Separation Logic
This paper proposes a modal extension of Separation Logic [8, 11] 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.
Susumu Nishimura
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where AMAST
Authors Susumu Nishimura
Comments (0)
books