首页 | 本学科首页   官方微博 | 高级检索  
     


A Proof of GMP Square Root
Authors:Yves Bertot  Nicolas Magaud  Paul Zimmermann
Abstract:We present a formal proof (at the implementation level) of an efficient algorithm proposed by P. Zimmermann in 1999 to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library, is completely proven within the COQ system. Proofs are developed using the CORRECTNESS tool to deal with imperative features of the program. The formalization is rather large (more than 13,000 lines) and requires some advanced techniques for proof management and reuse.
Keywords:arbitrary large numbers  formal methods  GMP  Coq
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号