Formal Modeling and Correctness Proof of Spatial Partition Algorithm. - Liping Zhu; Fangfang Wu; Pei Yang; Jixun Yan; Li Ma (CSDM Asia / CSDM, 2021)