[
https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17081007#comment-17081007
]
Julian Hyde commented on CALCITE-3913:
--------------------------------------
What form would the contribution take? Would you add a new test (and test
utilities to support it)? Would you add extra checks to existing tests (say
{{RelOptRulesTest}})?
I am excited to bring some formal methods into Calcite. Even if they are just
used for testing at first, people will be able to see them in use and may be
inspired to apply them in other ways.
> 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
> 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)
