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


SMT proof checking using a logical framework
Authors:Aaron Stump  Duckki Oe  Andrew Reynolds  Liana Hadarean  Cesare Tinelli
Affiliation:1. The University of Iowa, Iowa City, IA, USA
2. New York University, New York, NY, USA
Abstract:Producing and checking proofs from SMT solvers is currently the most feasible method for achieving high confidence in the correctness of solver results. The diversity of solvers and relative complexity of SMT over, say, SAT means that flexibility, as well as performance, is a critical characteristic of a proof-checking solution for SMT. This paper describes such a solution, based on a Logical Framework with Side Conditions (LFSC). We describe the framework and show how it can be applied for flexible proof production and checking for two different SMT solvers, clsat and cvc3. We also report empirical results showing good performance relative to solver execution time.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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