We show how, given a program and its separation logic proof,
one can parallelize and optimize this program and transform its proof simultaneously to obtain
a proven parallelized and optimized program.
To achieve this goal, we present new proof rules for generating proof trees
and a rewrite system on proof trees.
|Name||Lecture Notes in Computer Science|
|Conference||The 16th International Static Analysis Symposium, Los Angeles, USA|
|Period||9/08/09 → …|
- Separation Logic
- Proof-Preserving Optimizations
- Automatic Parallelization