You are viewing a plain text version of this content. The canonical link for it is here.
Posted to issues@calcite.apache.org by "Julian Hyde (Jira)" <ji...@apache.org> on 2020/04/10 22:24:00 UTC
[jira] [Updated] (CALCITE-3913) A formal verification techniques
for testing correctness in calcite
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]
Julian Hyde updated CALCITE-3913:
---------------------------------
Description:
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.
was:
Hi All,
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.
> 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)