[
https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17085315#comment-17085315
]
Julian Hyde commented on CALCITE-3913:
--------------------------------------
I assume that Z3 is java. What's the license? Is it on [Maven
Central|https://search.maven.org/]?
I envisage you adding {{.proveCorrect()}} after {{.check()}} in an existing
test such as [RelOptRulesTest.
testExtractJoinFilterRule|https://github.com/apache/calcite/blob/16c9c36f319b06ebcf1338f0e40e9de2ee912adf/core/src/test/java/org/apache/calcite/test/RelOptRulesTest.java#L416].
> 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)
