3 ms·
This was running user-facing, in production? Do you have any experience with scaling Z3? I'm thinking large problems running on many machines, contra many small
by csl 10y ago
This was running user-facing, in production? Do you have any experience with scaling Z3? I'm thinking large problems running on many machines, contra many small problems on many processes.
For some reason, I always imagined that SMT was used to verify stuff before putting it into production, but this opens up a whole new world of ideas for me.
- ahelwer 10y agoIt wasn't running as any sort of persistent service, if that's what you mean. It just ran during deployments to check output of old & new firewall generation methods for equivalence. Something like what you describe was implemented in an Azure system called SecGuru, which is sort of a generalized version of firewall comparison to check security rule enforcement. Here is the whitepaper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/secguru.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...