Skip to Main content Skip to Navigation
Conference papers

Proving Computational Geometry Algorithms in TLA+2

Hui Kong 1 Hehua Zhang 1 Xiaoyu Song 1 Ming Gu 1 Jiaguang Sun 2
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Geometric algorithms are widely used in many scientific fields like computer vision, computer graphics. To guarantee the correctness of these algorithms, it's important to apply formal method to them.We propose an approach to proving the correctness of geometric algorithms. The main contribution of the paper is that a set of proof decomposition rules is proposed which can help improve the automation of the proof of geometric algorithms. We choose TLA+2, a structural specification and proof language, as our experiment environment. The case study on a classical convex hull algorithm shows the usability of the method.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Hehua Zhang <>
Submitted on : Friday, July 29, 2011 - 7:04:08 AM
Last modification on : Tuesday, June 1, 2021 - 2:34:07 PM
Long-term archiving on: : Monday, November 7, 2011 - 11:34:13 AM


Files produced by the author(s)


  • HAL Id : inria-00612413, version 1



Hui Kong, Hehua Zhang, Xiaoyu Song, Ming Gu, Jiaguang Sun. Proving Computational Geometry Algorithms in TLA+2. 5th IEEE International Conference on Theoretical Aspects of Software Engineering(TASE 2011), Aug 2011, Xi'an, China. ⟨inria-00612413⟩



Record views


Files downloads