5 ms·

Is this still useful for managed languages? What is a practical use case for this for a Java/python web app?

• dons 8y ago
  Solving NP hard problems efficiently.
  • amelius 8y ago
    I know that every NP problem can be written as an SMT problem, theoretically speaking. But is that actually practical?
    • KirinDave 8y ago
      The answer to that question is, "Yes, if your SMT solver has strategies that provide good results for the problem in question." Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.
• spawarotti 8y ago
  Z3 is used by IntelliTest: https://docs.microsoft.com/en-us/visualstudio/test/generate-unit-tests-for-your-code-with-intellitest?view=vs-2017 https://docs.microsoft.com/en-us/visualstudio/test/generate-... You can use it to answer questions like "I want to reach this statement in this C# method, what values this method's inputs have to have for the execution to pass all the if checks and so on to reach this statement?". More broadly speaking, you can use Z3 as a solver for Dynamic Symbolic Execution engine, where DSE is described in: https://www.microsoft.com/en-us/research/publication/deconstructing-dynamic-symbolic-execution/ https://www.microsoft.com/en-us/research/publication/deconst... Source: I am the first author of "Generating Test Suites with Augmented Dynamic Symbolic Execution" leveraging Z3: https://www.microsoft.com/en-us/research/wp-content/uploads/2013/06/paper_tap13.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...