A one day workshop on using SMT-Solvers and bounded model checker for reverse engineering and binary analysis.