4 ms·

Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a lif

Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.

enz 8y ago
Z3 seems cool and I want to try but I must admit I fail to see how to use it for a real world project. Do you have a blog post talking about your Z3 use for your project?
- saurabh20n 8y ago
  The below were written for a semi- or non-technical audience, and only address your curiosity tangentially, but better than nothing: * Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-program-synthesis-101-294a9a35177 https://medium.com/@vidiborskiy/software-writes-software-pro... * Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-contract-security-101-d708002b2198 https://medium.com/@vidiborskiy/program-synthesis-smart-cont... * Synthetic Minds (that is us): https://synthetic-minds.com/ https://synthetic-minds.com/ You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.
- dhash 8y ago
  We at Radix Labs (S18) use Z3 (and CVC4/SyGuS) heavily as a library to solve place-and-route problems for goal directed robot path planning problems. Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these. With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in [1]), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment. A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. [2] It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP [3]. check out their instances to see how people really use them. [1] https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form... [2] https://www.trailofbits.com/services/blockchain-security/ https://www.trailofbits.com/services/blockchain-security/ [3] http://smtcomp.sourceforge.net/2018/ http://smtcomp.sourceforge.net/2018/
  - saurabh20n 8y ago
    Trail of bits is not building anything in program synthesis.
OxO4 8y ago
Out of curiosity, what made you choose Z3 over other SMT solvers? Also, if you have benchmarks that you can publish, it would be really great if you could submit them to SMT-LIB/SMT-COMP [0] such that they can be used to improve SMT solvers. [0] https://smt-comp.github.io/news/2019-01-24.html https://smt-comp.github.io/news/2019-01-24.html
- saurabh20n 8y ago
  About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances. Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.) --- [1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/tree/master/VS3 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers" [2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/blob/master/VS3/VS3-benchmark-A10.smt2 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... [3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis-9pt.pdf#page=146 http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...

Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.

enz 8y ago

Z3 seems cool and I want to try but I must admit I fail to see how to use it for a real world project. Do you have a blog post talking about your Z3 use for your project?

saurabh20n 8y ago
The below were written for a semi- or non-technical audience, and only address your curiosity tangentially, but better than nothing: * Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-program-synthesis-101-294a9a35177 https://medium.com/@vidiborskiy/software-writes-software-pro... * Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-contract-security-101-d708002b2198 https://medium.com/@vidiborskiy/program-synthesis-smart-cont... * Synthetic Minds (that is us): https://synthetic-minds.com/ https://synthetic-minds.com/ You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.
dhash 8y ago
We at Radix Labs (S18) use Z3 (and CVC4/SyGuS) heavily as a library to solve place-and-route problems for goal directed robot path planning problems. Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these. With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in [1]), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment. A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. [2] It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP [3]. check out their instances to see how people really use them. [1] https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form... [2] https://www.trailofbits.com/services/blockchain-security/ https://www.trailofbits.com/services/blockchain-security/ [3] http://smtcomp.sourceforge.net/2018/ http://smtcomp.sourceforge.net/2018/
- saurabh20n 8y ago
  Trail of bits is not building anything in program synthesis.

OxO4 8y ago

Out of curiosity, what made you choose Z3 over other SMT solvers? Also, if you have benchmarks that you can publish, it would be really great if you could submit them to SMT-LIB/SMT-COMP [0] such that they can be used to improve SMT solvers. [0] https://smt-comp.github.io/news/2019-01-24.html https://smt-comp.github.io/news/2019-01-24.html

saurabh20n 8y ago
About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances. Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.) --- [1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/tree/master/VS3 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers" [2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/blob/master/VS3/VS3-benchmark-A10.smt2 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... [3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis-9pt.pdf#page=146 http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...