Name
Abstract | ||
|---|---|---|
Parallel programming is rapidly gaining importance as a vec- tor 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 memory. 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, provided the specification and the proof of the original program are strengthened by certifying analyzers, an extension of program analyzers that produce a derivation that the results of the analysis are correct. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-89330-1_6 | Asian Symposium on Programming Languages and Systems |
Keywords | Field | DocType |
abstract interpretation,compositional proof system,parallel divide-and-conquer program,sequoia program,parallel programming,provably correct sequoia program,certified reasoning,parallel program,memory hierarchies,improved capability,high performance application,common program optimizations,computer architecture,program optimization,tree structure,divide and conquer | Programming language,Memory hierarchy,Computer science,Abstract interpretation,Exploit,Theoretical computer science,Sequoia,Proof obligation,Hierarchy,Certification | Conference |
Volume | ISSN | Citations |
5356 | 0302-9743 | 2 |
PageRank | References | Authors |
0.36 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| César Kunz | 2 | 167 | 10.81 |
| Jorge Luis Sacchini | 3 | 20 | 3.24 |
| inria sophia antipolismediterranee | 4 | 2 | 0.36 |