[
https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17085257#comment-17085257
]
Qi Zhou commented on CALCITE-3913:
----------------------------------
Hi,
I think the first step I can do is trying to add the code that only supports
logical join with inner join, logical table scan, logical filter and logical
projections with limited support for rex node, basically, SPJ queries. And I
can use the tool as a correctness test for test cases in
core/src/test/resources/org/apache/calcite/test/RelOptRulesTest.xml. Since I am
new to this, what is the next step I should do if I want to push some code into
calcite to make this happen? Also since my tool is based on Z3, which is an
open-source SMT solver that is developed by Microsoft, is it ok for using it?
Thank you for helping me!
> Test correctness using formal verification techniques
> -----------------------------------------------------
>
> Key: CALCITE-3913
> URL: https://issues.apache.org/jira/browse/CALCITE-3913
> Project: Calcite
> Issue Type: Wish
> Reporter: Qi Zhou
> Priority: Major
>
> 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)
