01
Z3 and SMT: Making Automated Reasoning a Software Engineering Component
Z3 helped make satisfiability modulo theories a reusable verification engine, combining Boolean search with theory reasoning so software tools could ask rich logical questions about arithmetic, arrays, bit-vectors and programs.
↗