Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance in the analysis of safety-critical systems, e. g., in the au...
详细信息
ISBN:
(纸本)9781424497560
Symbolic methods in computer-aided verification rely heavily on constraint solvers. The correctness and reliability of these solvers are of vital importance in the analysis of safety-critical systems, e. g., in the automotive context. Satisfiability results of a solver can usually be checked by probing the computed solution. This is in general not the case for unsatisfiability results. In this paper, we propose a certification method for unsatisfiability results for mixedboolean and nonlinear arithmetic constraintformulae. Such formulae arise in the analysis of hybrid discrete/continuous systems. Furthermore, we test our approach by enhancing the iSAT constraint solver to generate unsatisfiability proofs, and implemented a tool that can efficiently validate such proofs. Finally, some experimental results showing the effectiveness of our techniques are given.
暂无评论