diff --git a/copilot-cbmc.cabal b/copilot-cbmc.cabal
--- a/copilot-cbmc.cabal
+++ b/copilot-cbmc.cabal
@@ -1,8 +1,8 @@
 cabal-version             : >= 1.10
 name                      : copilot-cbmc
-version                   : 0.1
-synopsis                  : .
-description               : .
+version                   : 0.2
+synopsis                  : Copilot interface to a C model-checker.
+description               : Depends on CBMC <http://www.cprover.org/cbmc/>.  Generates a driver to prove the Atom and SBV backends generate equivalent code.
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : leepike@galois.com
@@ -12,8 +12,6 @@
 extra-source-files        : README.md
 
 author                    : Lee Pike
-                          , Robin Morisset
-                          , Alwyn Goodloe
                           , Sebastian Niller
                           , Nis Nordby Wegmann
 
diff --git a/src/Copilot/Tools/CBMC.hs b/src/Copilot/Tools/CBMC.hs
--- a/src/Copilot/Tools/CBMC.hs
+++ b/src/Copilot/Tools/CBMC.hs
@@ -4,7 +4,14 @@
 
 {-# LANGUAGE GADTs #-}
 
-module Copilot.Tools.CBMC (Params (..), defaultParams, genCBMC) where
+module Copilot.Tools.CBMC 
+  ( Params (..)
+  , defaultParams
+  , genCBMC
+  , atomPrefix
+  , sbvPrefix
+  , appendPrefix
+  ) where
 
 import Copilot.Core
 import qualified Copilot.Compile.C99 as C99
@@ -12,39 +19,48 @@
 import qualified System.IO as I
 import Text.PrettyPrint.HughesPJ
 
+--------------------------------------------------------------------------------
+
 data Params = Params
   { numIterations :: Int }
 
+--------------------------------------------------------------------------------
+
 defaultParams :: Params
 defaultParams = Params
   { numIterations = 10 }
 
+--------------------------------------------------------------------------------
+
+atomPrefix, sbvPrefix :: Maybe String
+atomPrefix = Just "atm"
+sbvPrefix = Just "sbv"
+
+appendPrefix :: Maybe String -> String -> String
+appendPrefix (Just pre) name = pre ++ "_" ++ name
+appendPrefix Nothing name = name
+
+--------------------------------------------------------------------------------
+
 genCBMC :: Params -> Spec -> IO ()
 genCBMC params spec =
   do
-    C99.compile (C99.defaultParams { C99.prefix = Just "atm" }) spec
-    SBV.compile (SBV.defaultParams { SBV.prefix = Just "sbv" }) spec
+    C99.compile (C99.defaultParams { C99.prefix = atomPrefix }) spec
+    SBV.compile (SBV.defaultParams { SBV.prefix = sbvPrefix }) spec
     h <- I.openFile "cbmc_driver.c" I.WriteMode
     I.hPutStrLn h (render (driver params spec))
 
+--------------------------------------------------------------------------------
+
 driver :: Params -> Spec -> Doc
 driver Params { numIterations = k } spec = vcat
   [ text "#include <stdbool.h>"
   , text "#include <stdint.h>"
-  , text "#include \"atm_copilot.h\""
-  , text "#include \"sbv_copilot/sbv_copilot.h\""
+  , text "#include <assert.h>"
+  , include atomPrefix C99.c99DirName C99.c99FileRoot
+  , include sbvPrefix SBV.sbvDirName "copilot"
   , text ""
-  , text "int32_t nondet_bool();"
-  , text "int32_t nondet_uint8_t();"
-  , text "int32_t nondet_uint16_t();"
-  , text "int32_t nondet_uint32_t();"
-  , text "int32_t nondet_uint64_t();"
-  , text "int32_t nondet_int8_t();"
-  , text "int32_t nondet_int16_t();"
-  , text "int32_t nondet_int32_t();"
-  , text "int32_t nondet_int64_t();"
-  , text "int32_t nondet_float();"
-  , text "int32_t nondet_double();"
+  , declNonDets spec
   , text ""
   , declExterns spec
   , text ""
@@ -59,8 +75,8 @@
   , text "  for (i = 0; i < " <> int k <> text "; i++)"
   , text "  {"
   , text "    sampleExterns();"
-  , text "    atm_step();"
-  , text "    sbv_step();"
+  , text $ "    " ++ appendPrefix atomPrefix "step();"
+  , text $ "    " ++ appendPrefix sbvPrefix "step();"
   , text "    verify_observers();"
   , text "  }"
   , text ""
@@ -68,13 +84,35 @@
   , text "}"
   ]
 
+  where
+  include prefix dir header = text "#include" <+> doubleQuotes
+     (   text (appendPrefix prefix dir) <> text"/" 
+      <> text (appendPrefix prefix (header ++ ".h"))
+     )
+
+--------------------------------------------------------------------------------
+
+declNonDets :: Spec -> Doc
+declNonDets = vcat . map declNonDet . externVars
+  where
+  declNonDet :: ExtVar -> Doc
+  declNonDet ext@(ExtVar _ t) = typeSpec t <+> nonDetName ext 
+
+--------------------------------------------------------------------------------
+
+nonDetName :: ExtVar -> Doc
+nonDetName (ExtVar name t) = 
+  text ("nondet_" ++ name ++ "_") <> (typeSpec t) <> text "();"
+
+--------------------------------------------------------------------------------
+
 declExterns :: Spec -> Doc
 declExterns = vcat . map declExtern . externVars
-
   where
+  declExtern :: ExtVar -> Doc
+  declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
 
-    declExtern :: ExtVar -> Doc
-    declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
+--------------------------------------------------------------------------------
 
 sampleExterns :: Spec -> Doc
 sampleExterns spec = vcat
@@ -86,10 +124,11 @@
   ]
 
   where
+  sampleExtern :: ExtVar -> Doc
+  sampleExtern ext@(ExtVar name _) =
+    text name <+> text "=" <+> nonDetName ext
 
-    sampleExtern :: ExtVar -> Doc
-    sampleExtern (ExtVar name t) =
-      text name <+> text "=" <+> text "nondet_" <> typeSpec t <> text "();"
+--------------------------------------------------------------------------------
 
 verifyObservers :: Spec -> Doc
 verifyObservers spec = vcat
@@ -101,17 +140,16 @@
   ]
 
   where
+  verifyObserver :: Observer -> Doc
+  verifyObserver (Observer name _ _) =
+    text "assert(" <> text (appendPrefix atomPrefix name) <+> text "==" 
+      <+> text (appendPrefix sbvPrefix name) <> text ");"
 
-    verifyObserver :: Observer -> Doc
-    verifyObserver (Observer name _ _) =
-      text "assert(" <> text "atm_" <> text name <+> text "==" <+> text "sbv_" <>
-      text name <> text ");"
+--------------------------------------------------------------------------------
 
 typeSpec :: UType -> Doc
 typeSpec UType { uTypeType = t } = text (typeSpec' t)
-
   where
-
   typeSpec' Bool   = "bool"
   typeSpec' Int8   = "int8_t"
   typeSpec' Int16  = "int16_t"
@@ -123,3 +161,5 @@
   typeSpec' Word64 = "uint64_t"
   typeSpec' Float  = "float"
   typeSpec' Double = "double"
+
+--------------------------------------------------------------------------------