Patent ID: 8180786
Filing Date: 2012-05-15
Classification: G06F

Abstract:
1. A method for evaluating a database, the method implemented by a computing device and comprising: receiving input information, the input information including: generating output information based on the input information using a satisfiability modulo theories (SMT) approach, the output information including: populating the database with the table information to provide a populated database; instantiating the query with the parameter information to provide an instantiated query; submitting the instantiated query to the populated database and receiving an evaluation result; and comparing the evaluation result with the condition information to provide an evaluation assessment, wherein the table information and the query information are provided such that, when the instantiated query is submitted to the populated database, the evaluation result agrees with the condition information; wherein said generating comprises: translating the query into a formula based on a background theory, wherein the formula is expressed within the background theory; preprocessing the formula to render the formula in a form suitable for processing by a SMT solver module; and processing the formula, after said preprocessing, using the SMT solver module to generate a model using the SMT approach.