Design errors in computer systems, i.e. bugs, can cause inconvenience, loss of data and time, and in some cases catastrophic damages. One approach for improving design correctness is formal methods: techniques aiming at mathematically establishing that a piece of hardware or software satisfies certain properties. For some industrial cases in which formal methods are utilized, a huge number of extremely large mathematical formulas are generated and checked for satisfiability. For these applications, high-performance solvers, which automatically check the formulas, play a crucial role.;For example, propositional logic (SAT) solvers are very popular. However, it is rather expensive to encode certain problems in propositional logic and the encoding is tricky and hard to understand. Recently, Satisfiability Modulo Theories (SMT) solvers have been developed to handle formulas in a more expressive first order logic. In contrast to general theorem provers that check satisfiability under all models, SMT solvers check satisfiability with regard to some background theories, such as theories of arithmetic, arrays and bit-vectors. SMT solvers are efficient and automatic like SAT solvers, while accepting much more general formulas.;For some applications, SMT formulas with quantifiers are useful. Traditional SMT solvers only consider quantifier-free formulas. In general, deciding SMT formulas containing quantifiers is undecidable. In other words, there are no complete and sound algorithms for solving a quantified SMT formulas.;This dissertation proposes several novel techniques for solving quantified SMT formulas. For general quantifier reasoning in SMT, the practical approach adopted by most state-of-the-art SMT solvers is heuristics-based instantiation. We propose a number of new heuristics. Most important is the notion of "instantiation level" that solves several challenges of general quantifier reasoning at the same time. These new heuristics have been implemented in solver CVC3, and experimental results show that a significant number of additional benchmarks can be solved than could be solved by CVC3 before.;When only considering formulas restricted to be within certain fragments of first order logic, it is possible to have complete algorithms based on instantiation. We propose a series of new fragments, and prove that formulas in these new fragments can be solved by complete algorithm based on instantiation.;Finally, this dissertation addresses the correctness of solvers. A practical method to improve correctness is to ask an SMT solver to produce a proof for a case it solves, and then proceed to check the proof. The problem is that such a proof checker will be rather complicated because it has to deal with a lot of proof rules. Thus the correctness of the proof checker becomes questionable. We propose a proof translator that translates a proof from SMT solver CVC3 into a trusted solver HOL Light. Experimental results show that this approach is feasible. When translating proofs, two faulty proof rules in CVC3 and two mis-labeled benchmarks in SMT-LIB were discovered.
展开▼
