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


SAT Modulo Linear Arithmetic for Solving Polynomial Constraints
Authors:Cristina Borralleras  Salvador Lucas  Albert Oliveras  Enric Rodríguez-Carbonell  Albert Rubio
Affiliation:1. Universitat de Vic, Vic, Spain
2. Universitat Polit??cnica de Val??ncia, Val??ncia, Spain
3. Universitat Polit??cnica de Catalunya, Barcelona, Spain
Abstract:Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g., termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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