Quantifier Elimination for Database Driven Verification

Technical Report, arXiv.org e-Print archive. CoRR Technical Report arXiv:1806.09686 2018. Available at https://arxiv.org/abs/1806.09686.

Running verification tasks in database driven systems requires solving quantifier elimination problems (not including arithmetic) of a new kind. In this paper, we supply quantifier elimination algorithms based on Knuth-Bendix completions and begin studying the complexity of these problems, arguing that they are much better behaved than their arithmetic counterparts. This observation is confirmed by analyzing the preliminary results obtained using the MCMT tool on the verification of data-aware process benchmarks. These benchmarks can be found in the last version of the tool distribution.

@techreport{Corr-2018-qeddv,
   title = "Quantifier Elimination for Database Driven Verification",
   year = "2018",
   author = "Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and
Marco Montali and Andrey Rivkin",
   institution = "arXiv.org e-Print archive",
   number = "arXiv:1806.09686",
   note = "Available at https://arxiv.org/abs/1806.09686",
}