3 ms·

Thanks again. I didn't know Z3 could handle formulae with real numbers. I will take a closer look at it. :) On the network firewall rules (at multi-tenant Az

by xtacy 11y ago

Thanks again. I didn't know Z3 could handle formulae with real numbers. I will take a closer look at it. :) On the network firewall rules (at multi-tenant Azure, I presume), what were Z3's runtimes look like?

ahelwer 11y ago
Z3 was able to check equivalence of firewalls with a few hundred rules in a fraction of a second on a standard workstation. I was extremely impressed, especially since the brute-force IPv4 packet search space is 2^112! There's some wizardry going on beneath the hood.