Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

7

CADE
2006
Springer

favoriteEmaildiscussreport

102views Logical Reasoning» more CADE 2006»

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials

14 years 5 months ago

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials

Download www.lix.polytechnique.fr

We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result.

Assia Mahboubi

Real-time Traffic

Automated Reasoning | CADE 2006 | Mechanized Proof |

claim paper

Related Content

» Constraint Bipartite Vertex Cover Simpler Exact Algorithms and Implementations

» Slicing communicating automata specifications polynomial algorithms for model reduction

» Componentlevel parallelization of triangular decompositions

» Do You Trust Your Model Checker

» Zero knowledge with efficient provers

» Solving Nonlinear Polynomial Arithmetic via SAT Modulo Linear Arithmetic

» Design implementation and evaluation of a practical pseudoknot folding algorithm based on ...

» Efficient Massive Sharing of Content among Peers

» SAT and ATPG Boolean engines for formal hardware verification

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2006
Where	CADE
Authors	Assia Mahboubi

Comments (0)