Experimental Assessment And Capability Extension Of Smt Solvers

Formal method has been proven to be an effective technique in verifying the trustness of software and hardware systems, and it includes several applicable methods such as model checking, theory proving, equivalence checking as well as language containment. Many of these formal methods can be translated to Boolean/Propositional Satisfiability Problems (SAT), which is used to decide whether a formula according to propositional logic is satisfied. SAT is well-known as the first proved NP-Complete problem. Compared with SAT, Satisfiable Module Theories (SMT) problems are more expressive and abstractive, thus SMT becomes critical problems in verification field. This thesis mainly focuses on two things, one is to make sure of the state-of-the-art abilities of SMT solvers, and the other is to find a way to enlarge and complement the capabilities of SMT solvers.SMT problem belongs to first-order logic and its decidable theories ranges over fields as equalities and uninterpreted functions, linear arithmetic, bitvectors as well as quantified problems. However, combination of mutiple theories is considered to be with great applicable values due to the demands of the presently complex and multi-era industrial applications. This article comparatively analyzes three of theory combination techniques: Nelson-Oppen, Delayed Theory Combination and Ackermann methods. Besides, we present the newest techniques for SMT solvers in dealing with thoery combination, and then a capabilities envaluation platform totally oriented to real-world applications for SMT solvers is given, we comparatively testing the latest and usable verisions of five SMT solvers. Through the results, we can find out that Z3 beats others for the whole performance with the refined DTC approach based on model, especially in dealing with quatified formulas.Not all the theory domains SMT solvers have got a complete decidable method; there are still some unsolvable SMT problems, especially the quantified problems. This article shows a generalized formula pattern which SMT slovers can not solve at present. A new method for solving this formula pattern is proposed, we construct a symbolic form of automata, and the correctness of this translating process has been proved in this article. Finally, we realize a complete decision procedure for quantified SMT formula, which combines our translating program with the input parser module and language decision technique of automata. Results prove our new method is feasiblible; besides, it strengthens the capability of SMT solvers and makes contributions both to theoreticle meanings and applicatible values.