Model Extraction: Several program model checkers are based on automated model extraction, where program is translated into an input notation of an existing model checker (Corbett 1998; Havelund and Pressburger 2000; Corbett et al. 2000; Ball et al. 2001; Holzmann and Smith 2002). Bandera (Corbett et al. 2000) translates Java programs to a number of back-end model checkers, including SPIN (Holzmann 2004), dSPIN (dSPIN website), SMV (SMV website), Bogor (Robby, Dwyer, and Hatcliff 2003), and Java PathFinder (JPF) (JPF website). Bandera also supports abstraction by transforming the Java programs to "abstract" Java programs which are then translated. JCAT (JCAT website) translates Java to SPIN and dSPIN. FeaVer/Modex (FeaVer website, Modex website) translates C code to SPIN. FeaVer and SLAM incorporate abstraction methods into the translation process. FeaVer's abstraction is semi-automated, while SLAM uses predicate abstraction and abstraction refinement (Ball, Podelski, and Rajamani 2002) to automate abstraction during model checking.