Certified Reasoning in Memory Hierarchies

Abstract. Parallel programming is rapidly gaining importance as a vector to develop high performance applications that exploit the improved capabilities of modern computer architectures. In consequence, there is a need to develop analysis and verification methods for parallel programs. Sequoia is a language designed to program parallel divide-and-conquer programs over a hierarchical, tree-structured, and explicitly managed Using abstract interpretation, we develop a compositional proof system to analyze Sequoia programs and reason about them. Then, we show that common program optimizations transform provably correct Sequoia programs into provably correct Sequoia programs.

• Type: Conference
• Year: 2008
• Where: APLAS
• Authors: Gilles Barthe, César Kunz, Jorge Luis Sacchini
• Keywords: APLAS 2008, Correct Sequoia Programs, Programming Languages, Provably Correct, Sequoia Programs