To explore Z3 projects, I sometimes just browse the tags on Github [0]. I also am not aware of a better way to get an overview. However, I know Z3 is used a lot in industry for verification and resource allocation tasks.
Personally, I have made extensive use of Z3 to find bugs in domain-specific language (DSL) compilers [1]. You can use Z3 to encode the source code before and after a compiler optimization as a logic formula and then check whether the formulae are equivalent. If they are not, there is likely a semantic bug in the transformation pass of your compiler, meaning you have introduced a subtle logic mistake.
This style of verification really works best if your programming language is sufficiently restricted (not Turing-complete) or if you pick isolated segments in your code (e.g., functions). If that is the case, these methods can be extremely effective. We have found many semantic bugs in a short time period. In our case, Z3 was not even the bottleneck, performance-wise. It was our language interpreter. And because the language is sufficiently restricted, we can even run our tool as part of the compiler CI. So whenever a pull request is made, we can check whether it may lead to subtle issues in program translation.
Another useful aspect of using Z3 to represent a programming language is that you can also generate test cases for your programs. As far as I know, the Rosette [2] framework is intended to make all of this more approachable.
Comments
To explore Z3 projects, I sometimes just browse the tags on Github [0]. I also am not aware of a better way to get an overview. However, I know Z3 is used a lot in industry for verification and resource allocation tasks.
Personally, I have made extensive use of Z3 to find bugs in domain-specific language (DSL) compilers [1]. You can use Z3 to encode the source code before and after a compiler optimization as a logic formula and then check whether the formulae are equivalent. If they are not, there is likely a semantic bug in the transformation pass of your compiler, meaning you have introduced a subtle logic mistake.
This style of verification really works best if your programming language is sufficiently restricted (not Turing-complete) or if you pick isolated segments in your code (e.g., functions). If that is the case, these methods can be extremely effective. We have found many semantic bugs in a short time period. In our case, Z3 was not even the bottleneck, performance-wise. It was our language interpreter. And because the language is sufficiently restricted, we can even run our tool as part of the compiler CI. So whenever a pull request is made, we can check whether it may lead to subtle issues in program translation.
Another useful aspect of using Z3 to represent a programming language is that you can also generate test cases for your programs. As far as I know, the Rosette [2] framework is intended to make all of this more approachable.
[0]https://github.com/search?q=topic%3Az3&type=Repositories [1]https://www.usenix.org/conference/osdi20/presentation/ruffy [2]https://emina.github.io/rosette/