Browse files

documentation updates.

  • Loading branch information...
1 parent d1e7f92 commit cad2ac75655361d73efa42b3b6b8ae4bd499acb4 @leepike leepike committed Sep 30, 2011
Showing with 50 additions and 7 deletions.
  1. +46 −7
  2. +4 −0 copilot-cbmc.cabal
@@ -1,18 +1,57 @@
+[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.
+Please see the files under the Examples directory in the
+[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.
+The Copilot library is cabalized. Assuming you have cabal and the GHC compiler
+installed (the [Haskell 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
+copilot-cbmc depends on the C model-checker, CBMC.
+[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.
+[copilot-cbmc]( is available on
-We are grateful for NASA Contract NNL08AD13T to [Galois, Inc]( and the [National Institute of Aerospace](, which partially supported this work.
+**Sources** for each package are available on Github as well. Just go to
+[Github]( 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]( verbiage.
-Copilot is distributed under a BSD3 license. The license terms are stated in the [LICENSE](
+We are grateful for NASA Contract NNL08AD13T to [Galois,
+Inc]( and the [National Institute of
+Aerospace](, which partially supported this work.
@@ -17,6 +17,10 @@ author : Lee Pike
, Sebastian Niller
, Nis Nordby Wegmann
+source-repository head
+ type: git
+ location: git://
default-language : Haskell2010
hs-source-dirs : src

0 comments on commit cad2ac7

Please sign in to comment.