Network Verification

Here you can find all the code and benchmarks related to our network verification effort.

Downloads

• Stanford benchmarks: stanford_bench.tar.bz2. Topology from Hassel.
• Cloud benchmarks: cloud_bench.tar.bz2.
• Our Z3 fork containing the BDD, union of cubes, and difference of cubes Datalog backends is available from CodePlex.
• Misc scripts, including our Cloud topology generator, a .tf to .smt2 converter, a .tf to .dot converter, and our All SAT implementation for .tf files.

Benchmark Results

Run times for multiple Z3 μZ solvers.

Usage Instructions

1) Obtain Z3 from CodePlex and checkout the "unstable" branch.

2) Compile Z3: ./configure && cd build && make

3) Running benchmarks:

• BDDs: z3 fixedpoint.engine=datalog fixedpoint.default_relation=bdd_relation fixedpoint.similarity_compressor=false fixedpoint.unbound_compressor=false file.smt2
• BMC: z3 fixedpoint.engine=bmc fixedpoint.similarity_compressor=false file.smt2
• CLP: z3 fixedpoint.engine=clp file.smt2
• Union of cubes: z3 fixedpoint.engine=datalog fixedpoint.default_relation=hassel fixedpoint.similarity_compressor=false file.smt2
• Difference of cubes: z3 fixedpoint.engine=datalog fixedpoint.default_relation=hassel_diff fixedpoint.unbound_compressor=false file.smt2
• PDR: z3 fixedpoint.engine=pdr fixedpoint.bit_blast=true fixedpoint.unbound_compressor=false file.smt2

Note: Unfortunately, CodePlex is not on-line anymore. The official Z3 distribution has a new implementation of the difference of cubes backend, which can be used with: fixedpoint.default_relation=doc. The BDD backend was lost and it is not available in the official Z3 distribution.