Philip Zucker is a physics and computer science enthusiast documenting ideas and experiments in a lab-notebook-style blog, focused on functional programming, compilers, formal methods, and scientific computation.
25 articles from this blog
Explores combining SMT solvers CVC5 and Z3 using the Nelson-Oppen method, focusing on theory combination and purification.
Explores asymmetric completion, a union-find algorithm variant for inequality reasoning, with Python implementation insights.
Introducing a Lean-like syntax parser for the Knuckledragger theorem prover to improve formula readability over verbose Python/Z3Py syntax.
Exploring a semi-interactive proof system for verifying assembly code using Python, Z3, and Ghidra Pcode.
A technical exploration of building a toy DPLL SAT solver in Python, discussing its implementation and relation to SMT solvers.
