diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+2009
+BSD3 License terms
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+Neither the name of the developers nor the names of its contributors
+may be used to endorse or promote products derived from this software
+without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,57 @@
+Overview
+========
+[copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to
+generate a driver using CBMC, a third-party tool (see Dependencies below) that
+proves that the code generated by different C back-ends is equivalent.
+Currently, this includes the C99 back-end and the SBV back-end.
+
+Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
+Haskell that compiles into embedded C.  Copilot is similar in spirit to
+languages like Lustre.  Copilot contains an interpreter, multiple back-end
+compilers, and other verification tools.
+
+Examples
+=========
+Please see the files under the Examples directory in the
+[Copilot](http://hackage.haskell.org/package/copilot) for a number of examples
+showing the syntax, use of libraries, and use of the interpreter and back-ends.
+The examples is the best way to start.
+
+Installation
+============
+The Copilot library is cabalized. Assuming you have cabal and the GHC compiler
+installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the
+easiest way to obtain these), it should merely be a matter of running 
+     
+         cabal install copilot-cbmc
+
+However, we strongly recommend you install Copilot, which installs copilot-c99
+and other packages automatically.  Execute
+
+         cabal install copilot
+
+Dependencies
+=============
+copilot-cbmc depends on the C model-checker, CBMC.
+[CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code.  We
+use CBMC to prove that two back-ends generating C generate semantically
+equivalent C, to help detect bugs in C back-ends.
+
+Resources
+=========
+[copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) is available on
+Hackage.
+
+**Sources** for each package are available on Github as well.  Just go to
+[Github](github.com) and search for the package of interest.  Feel free to fork!
+
+Copyright, License
+==================
+Copilot is distributed with the BSD3 license. The license file contains the
+[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
+
+Thanks
+======
+We are grateful for NASA Contract NNL08AD13T to [Galois,
+Inc](http://corp.galois.com/) and the [National Institute of
+Aerospace](http://www.nianet.org/), which partially supported this work.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,21 @@
+module Main ( main ) where
+
+import System.Directory    (findExecutable)
+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, postInst)
+import System.Directory    (findExecutable)
+import System.Exit         (exitWith, ExitCode(..))
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks{ postInst = checkDefSolver }
+ where checkDefSolver _ _ _ _ = do
+                mbP <- findExecutable "cbmc"
+                case mbP of
+                   Nothing -> do putStrLn "***"
+                                 putStrLn "*** The copilot-cbmc library requires the solver cbcm to be installed."
+                                 putStrLn "*** The executable CBMC must be in your path."
+                                 putStrLn "*** Please install CBMC and put it in your path!"
+                                 putStrLn "*** CBMC can downloaded at http://www.cprover.org/cbmc/"
+                                 putStrLn "***"
+                   Just _  -> return ()
+                exitWith ExitSuccess
+
diff --git a/copilot-cbmc.cabal b/copilot-cbmc.cabal
new file mode 100644
--- /dev/null
+++ b/copilot-cbmc.cabal
@@ -0,0 +1,39 @@
+cabal-version             : >= 1.10
+name                      : copilot-cbmc
+version                   : 0.1
+synopsis                  : .
+description               : .
+license                   : BSD3
+license-file              : LICENSE
+maintainer                : leepike@galois.com
+stability                 : Experimental
+category                  : Language, Embedded
+build-type                : Custom
+extra-source-files        : README.md
+
+author                    : Lee Pike
+                          , Robin Morisset
+                          , Alwyn Goodloe
+                          , Sebastian Niller
+                          , Nis Nordby Wegmann
+
+source-repository head
+    type:       git
+    location:   git://github.com/niswegmann/copilot-cbmc.git
+
+library
+  default-language        : Haskell2010
+  hs-source-dirs          : src
+  ghc-options             : -Wall -fwarn-tabs
+  ghc-prof-options        : -auto-all -caf-all
+
+  build-depends           : base >= 4.3 && < 5
+                          , bytestring
+                          , copilot-core
+                          , directory >= 1.1
+                          , process >= 1.0
+                          , pretty
+                          , copilot-sbv
+                          , copilot-c99
+
+  exposed-modules         : Copilot.Tools.CBMC
diff --git a/src/Copilot/Tools/CBMC.hs b/src/Copilot/Tools/CBMC.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Tools/CBMC.hs
@@ -0,0 +1,125 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE GADTs #-}
+
+module Copilot.Tools.CBMC (Params (..), defaultParams, genCBMC) where
+
+import Copilot.Core
+import qualified Copilot.Compile.C99 as C99
+import qualified Copilot.Compile.SBV as SBV
+import qualified System.IO as I
+import Text.PrettyPrint.HughesPJ
+
+data Params = Params
+  { numIterations :: Int }
+
+defaultParams :: Params
+defaultParams = Params
+  { numIterations = 10 }
+
+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
+    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 ""
+  , 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();"
+  , text ""
+  , declExterns spec
+  , text ""
+  , sampleExterns spec
+  , text ""
+  , verifyObservers spec
+  , text ""
+  , text "int main (int argc, char const *argv[])"
+  , text "{"
+  , text "  int i;"
+  , text ""
+  , text "  for (i = 0; i < " <> int k <> text "; i++)"
+  , text "  {"
+  , text "    sampleExterns();"
+  , text "    atm_step();"
+  , text "    sbv_step();"
+  , text "    verify_observers();"
+  , text "  }"
+  , text ""
+  , text "  return 0;"
+  , text "}"
+  ]
+
+declExterns :: Spec -> Doc
+declExterns = vcat . map declExtern . externVars
+
+  where
+
+    declExtern :: ExtVar -> Doc
+    declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
+
+sampleExterns :: Spec -> Doc
+sampleExterns spec = vcat
+  [ text "void sampleExterns()"
+  , text "{"
+  , text ""
+  , nest 2 (vcat $ map sampleExtern (externVars spec))
+  , text "}"
+  ]
+
+  where
+
+    sampleExtern :: ExtVar -> Doc
+    sampleExtern (ExtVar name t) =
+      text name <+> text "=" <+> text "nondet_" <> typeSpec t <> text "();"
+
+verifyObservers :: Spec -> Doc
+verifyObservers spec = vcat
+  [ text "void verify_observers()"
+  , text "{"
+  , text ""
+  , nest 2 (vcat $ map verifyObserver (specObservers spec))
+  , text "}"
+  ]
+
+  where
+
+    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"
+  typeSpec' Int32  = "int32_t"
+  typeSpec' Int64  = "int64_t"
+  typeSpec' Word8  = "uint8_t"
+  typeSpec' Word16 = "uint16_t"
+  typeSpec' Word32 = "uint32_t"
+  typeSpec' Word64 = "uint64_t"
+  typeSpec' Float  = "float"
+  typeSpec' Double = "double"