Qi Zhou created CALCITE-3913:
--------------------------------
Summary: A formal verification techniques for testing correctness
in calcite
Key: CALCITE-3913
URL: https://issues.apache.org/jira/browse/CALCITE-3913
Project: Calcite
Issue Type: Wish
Reporter: Qi Zhou
Hi All,
We have developed a technique that can formally be verified if two logical
plans in calcite are indeed semantically equivalent. We published this paper in
VLDB 2019. Here is the link to the paper
+https://www.vldb.org/pvldb/vol12/p1276-zhou.pdf+. This technique converts two
logical plan into their symbolic representations and using an SMT
(Satisfiability modulo theories) solver to verify the relationship between two
symbolic representations to verify the equivalence. We are wondering if it is
possible that we can integrate this tool into calcite, as a way to help the
correctness testing process in calcite.
--
This message was sent by Atlassian Jira
(v8.3.4#803005)
