Michael Franz's dissertation: ftp://ftp.inf.ethz.ch/pub/publications/dissertations/th10497.ps.gz has a description of the techniques used, which may be useful in conjunction with the Juice code found in the github repos Colby linked to.