phone: +1-510-387-9419 (cell)



My current verification and synthesis framework, ZZ, is available at Bitbucket. MiniSat and SatELite now have their own page at All other software developed during my Ph.D. can be found in the package. More information and references can be found on the (now very out-dated) Satzoo page, and on the Tip (temporal induction prover) page.


During 1991-94, I created some Single Image Stereograms that are still somewhat popular, although quite low-res by today's standards. They used to take about 20 hours to generate by my 25 MHz 486sx.