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.
Type de document :
Communication dans un congrès
5th IEEE International Conference on Theoretical Aspects of Software Engineering(TASE 2011), Aug 2011, Xi'an, China. 2011
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00612413
Contributeur : Hehua Zhang <>
Soumis le : vendredi 29 juillet 2011 - 07:04:08
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : lundi 7 novembre 2011 - 11:34:13

Fichier

Proving_Computational_Geometry...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00612413, version 1

Collections

Citation

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. 2011. 〈inria-00612413〉

Partager

Métriques

Consultations de la notice

166

Téléchargements de fichiers

145