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


Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
Authors:Silvio Ranise,David D  harbe
Affiliation:aLORIA & INRIA-Lorraine, Nancy (France);bLORIA & INRIA-Lorraine, Nancy (France) and DIMAp/UFRN, Natal (Brazil)
Abstract:We describe a combination of BDDs and superposition theorem proving, called light-weight theorem proving, and its application to the flexible and efficient automation of the reasoning activity required to debug and verify pointer manipulating programs. This class of programs is notoriously challenging to reason about and it is also interesting from a programming point of view since pointers are an important source of bugs. The implementation of our technique (in a system called haRVey) scales up significantly better than state-of-the-art tools such as E (a superposition prover) and Simplify (a prover based on the Nelson and Oppen combination schema of decision procedures which is used in ESC/Java) on a set of proof obligations arising in debugging and verifying C functions manipulating pointers.
Keywords:
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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