Name
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. In this paper, 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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/TASE.2011.15 | TASE |
Keywords | Field | DocType |
algorithm verification,proof language,geometry algorithm,geometric algorithm,specification languages,convex hull algorithm,computer graphics,classical convex hull algorithm,computational geometry,case study,tla+2,proof decomposition rules,computational geometry algorithms,experiment environment,theorem proving,proof decomposition rule,computer vision,main contribution,proving computational geometry algorithms,loop invariant,formal method,structural specification language,convex hull,automation,computer graphic,silicon | Programming language,Computer science,Correctness,Computational geometry,Automated theorem proving,Convex hull,Algorithm,Theoretical computer science,Software,Loop invariant,Formal methods,Computer graphics | Conference |
ISBN | Citations | PageRank |
978-1-4577-1487-0 | 0 | 0.34 |
References | Authors | |
4 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hui Kong | 1 | 34 | 4.19 |
| Hehua Zhang | 2 | 109 | 12.65 |
| Xiaoyu Song | 3 | 318 | 46.99 |
| Ming Gu | 4 | 501 | 51.05 |
| Jia-guang Sun | 5 | 1807 | 134.30 |