[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17085361#comment-17085361 ]
Qi Zhou commented on CALCITE-3913: ---------------------------------- Z3 is not write in java, it is written in c++, but it has a java binding library. The license is MIT license. > 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)