Quantifier Elimination for Database Driven Verification
share
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. The content of this manuscript is very preliminary, its role being simply that of expanding the documentation available from MCMT v. 2.8 distribution.
READ FULL TEXT