Safe Smooth Paths Between Straight Line Obstacles

We describe a collections of algorithm to compute smooth trajectories between obstacles, with the objective that the obtained trajectories should be smooth. In particular, we use a vertical cell decomposition algorithm to avoid the obstacles, a best first search algorithm to obtain trajectory sketches and Bézier curves to implement smoothness. We also provide some insights into the correctness arguments for these algorithms. These correctness arguments are intended for use in a formal proof. While we have running implementations of the full program, the formal proofs of correctness are still incomplete.