Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 89 lines (67 sloc) 3.733 kb
8825a43 @leepike Starting README.
authored
1 Copilot: a stream DSL
2 ====================================
3 Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
4 Haskell that compiles into embedded C. Copilot is similar in spirit to
5 languages like Lustre. Copilot contains an interpreter, multiple back-end
abcdc2f @leepike Documentation updates.
authored
6 compilers, and other verification tools.
749f239 @leepike To build the package.
authored
7
8825a43 @leepike Starting README.
authored
8 Resources
9 =========
10 Copilot is comprised of a number of sub-projects which are automatically
11 installed when you install Copilot from Hackage, as described below:
12
13 * [copilot-language](http://hackage.haskell.org/package/copilot-language) The
14 front-end of Copilot defining the user language.
15
16 * [copilot-libraries](http://hackage.haskell.org/package/copilot-libraries)
17 User-supplied libraries for Copilot, including linear-temporal logic,
18 fault-tolerant voting, regular expressions, etc.
19
20 * [copilot-core](http://hackage.haskell.org/package/copilot-core) The core
21 language, which efficiently represents Copilot expressions. The core is only
22 of interest to implementers wishing to add a new back-end to Copilot.
23
24 * [copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to
25 generate a driver using CBMC, a third-party tool (see Dependencies below) that
26 proves that the code generated by different C back-ends is equivalent.
27 Currently, this includes the C99 back-end and the SBV back-end.
28
29 * [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that
30 translates to [Atom](http://hackage.haskell.org/package/copilot-cbmc) to
31 generate hard real-time C code.
32
33 Optionally, you may which also to install
34
35 * [copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end
36 that translates to [SBV](http://hackage.haskell.org/package/sbv), using its
37 code generator to generate hard real-time C code as well. The ad
38
abcdc2f @leepike Documentation updates.
authored
39 * [copilot-discussion](https://github.com/niswegmann/copilot-discussion)
8825a43 @leepike Starting README.
authored
40 Contains a tutorial, todos, and other items regarding the Copilot system.
41
abcdc2f @leepike Documentation updates.
authored
42 **Sources** for each package are available on Github as well. Just go to
43 [Github](github.com) and search for the package of interest. Feel free to fork!
44
8825a43 @leepike Starting README.
authored
45 Comments, bug reports, and patches are always welcome. Send them to leepike @
46 gmail.com
47
48 Examples
49 =========
abcdc2f @leepike Documentation updates.
authored
50 Please see the files under the Examples directory for a number of examples
8825a43 @leepike Starting README.
authored
51 showing the syntax, use of libraries, and use of the interpreter and back-ends.
52 The examples is the best way to start.
53
54 Installation
55 ============
56 The Copilot library is cabalized. Assuming you have cabal and the GHC compiler
57 installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the
58 easiest way to obtain these), it should merely be a matter of running
59
60 cabal install copilot
61
62 with an Internet connection. Please see the INSTALL file for installation
63 details.
64
65 Once the installation is done, you can run the executable `XXX` which will
66 execute the regression test suite for sbv on your machine.
67
68 Dependencies
69 =============
70 copilot-cbmc depends on the C model-checker, CBMC.
71 [CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code. We
72 use CBMC to prove that two back-ends generating C generate semantically
73 equivalent C, to help detect bugs in C back-ends.
74
75 Copyright, License
76 ==================
abcdc2f @leepike Documentation updates.
authored
77 Copilot is distributed with the BSD3 license. The license file contains the
78 [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
8825a43 @leepike Starting README.
authored
79
80 Thanks
81 ======
82 Copilot was developed, in part, with support from NASA's Aviation Safety
83 Program, Contract #NNL08AD13T. Copilot was developed jointly by Galois,
84 Inc. and the National Institute of Aerospace.
85
86 The following people have contributed to Copilot: Lee Pike, Nis Wegmann,
87 Sebastian Niller, Robin Morisset, Alwyn Goodloe, and Levent Erkok.
abcdc2f @leepike Documentation updates.
authored
88
Something went wrong with that request. Please try again.