4 ms·

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 you

by 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.

by 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.