[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

["Qi Zhou (Jira)" <ji...@apache.org>]

    [ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17148155#comment-17148155 ] 

Qi Zhou commented on CALCITE-3913:
----------------------------------

Hi,

 Sorry for the late actions. I try to submit my first PR that only adding the dependency for z3 and two simple tests to test if it works. I am a little bit confusing because this issue requires lots of code as the implementation. My next commit is trying to have code the can verify two filter condition (RexNode) returns the boolean result if given the same tuple. I feel like I have to decompose this issue into multiple commits, otherwise. It is impossible for the reviewer to review. 

 Thank you for helping!

Qi

> 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
>          Time Spent: 10m
>  Remaining Estimate: 0h
>
> 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)