new URL for “a dumb introduction to #Z3”. #formal-methods #toread
on 02026-06-07“a dumb introduction to #Z3”. #formal-methods #toread
on 02025-10-10Discussion of “a dumb introduction to #Z3” #formal-methods #toread
on 02025-10-10the main #documentation on how to use #Z3, including for #optimization #SAT #SMT
on 02024-06-23#Z3 #tutorial #documentation that covers things like validating numerical approximation algorithms and training neural networks with it #SAT #SMT
on 02024-06-23Leonardo de Moura’s #tutorial #documentation #introduction to #Z3 in Python. It starts out focusing on things like integers, real numbers, and arbitrary precision, but then moves on to bitvectors, bit-twiddling hacks, sudoku, N-queens, and package management. #SAT #SMT
on 02024-06-23#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16The "Z3++" #SMT solver, based on #Z3, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16The "Z3++" #SMT solver, based on #Z3, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16#PDF #paper about the #Z3++ #SMT solver, which is based on #Z3. #SAT #toread #formal-methods
on 02024-06-16#PDF #paper about the #Z3++ #SMT solver, which is based on #Z3. #SAT #toread #formal-methods
on 02024-06-16comments on an #introduction to the #Z3 #SAT #solver
on 02019-02-15#Z3 #formal-methods #tutorial #toread
on 02019-02-11John Regehr using #Z3 to prove that an integer cannot be simultaneously less than 2 and greater than 3.
on 02016-11-11