WG22/M15SolarLezama

Interactive derivation of provably correct divide-and-conquer dynamic programming implementations

In this talk I will describe a new approach to deductive synthesis based on 'solver-aided tactics' that combines the benefits of traditional deductive program derivation techniques with the strengths of constraint-based synthesis. We have applied this approach to the generation of complex divide-and-conquer implementations of dynamic programming algorithms. Divide-and-conquer implementations have been shown to have better locality and parallelism than traditional loop-based implementations, but they are difficult and error prone to construct by hand. The talk will show how our system based on solver-aided-tactics can support the derivation of provably correct implementations of these algorithms with only a small amount of user interaction.