* configure.ac: Remove doc/ from search path for Makefile.ams

* configure.ac, test/unit/Makefile.am: Resolved an issue where even
  when not testing, one unit test was built.

* Re-ran contrib/update-copyright.pl on all source files to ensure
  consistent and correct header comments.

* contrib/get-authors: Change definition of "minor contributor"
  to >= 10% of lines (rather than strictly greater than 10% of lines)

37 files changed, 106 insertions, 53 deletions

diff --git a/configure.ac b/configure.ac
index 8c1141b9d..d75ce6309 100644
--- a/configure.ac
+++ b/configure.ac
@@ -453,10 +453,16 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 mk_include=include
 AC_SUBST(mk_include)
 
+# CVC4_FALSE
+#
+# This is used to _always_ comment out rules in automake makefiles, but
+# still trigger certain automake behavior; see test/unit/Makefile.am.
+AM_CONDITIONAL([CVC4_FALSE], [false])
+
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 )
 
 AC_OUTPUT
diff --git a/contrib/get-authors b/contrib/get-authors
index a42f8a25b..40aaf6a6d 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -20,7 +20,7 @@ while [ $# -gt 0 ]; do
     ( while read lines author; do
         pct=$((100*$lines/$total_lines))
         if [ "$author" != "$original_author" ]; then
-          if [ $pct -gt 10 ]; then
+          if [ $pct -ge 10 ]; then
             major_contributors="${major_contributors:+$major_contributors, }$author"
           else
             minor_contributors="${minor_contributors:+$minor_contributors, }$author"
diff --git a/src/context/context.h b/src/context/context.h
index 1af4480f9..403235bc9 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -2,7 +2,7 @@
 /** context.h
  ** Original author: mdeters
  ** Major contributors: barrett
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 1d2705240..54500d0d5 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -1,7 +1,7 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** attribute.h
  ** Original author: mdeters
- ** Major contributors: dejan
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 18c0fdbab..c29b7e448 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** expr.cpp
  ** Original author: dejan
- ** Major contributors: taking
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/expr.h b/src/expr/expr.h
index dd4d0e9d7..096094aff 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -2,7 +2,7 @@
 /** expr.h
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, taking
+ ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 506c118bc..71368c101 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** expr_manager.cpp
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index edfc18c8d..d84cf76be 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** expr_manager.h
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 79490d58e..90dd86712 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node.cpp
  ** Original author: mdeters
- ** Major contributors: taking, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 12a6d1732..c6aee3dea 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node_manager.cpp
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 18a95f041..97f5ba9cd 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node_manager.h
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): taking, dejan
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h
index fe71a4d1a..0bf9b47cf 100644
--- a/src/expr/soft_node.h
+++ b/src/expr/soft_node.h
@@ -1,8 +1,8 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** soft_node.h
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index d4662d420..368a3fe44 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -1,5 +1,5 @@
-/*********************                                           -*- C++ -*-  */
-/** type.h
+/*********************                                                        */
+/** type.cpp
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): none
diff --git a/src/expr/type.h b/src/expr/type.h
index 19d0c831e..fd485602e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,8 +1,8 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** type.h
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 190f7bbf3..7ca889592 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -2,7 +2,7 @@
 /** getopt.cpp
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): barrett, dejan
+ ** Minor contributors (to current version): barrett, dejan, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 6ebe895a5..a12c69df7 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -2,7 +2,7 @@
 /** main.cpp
  ** Original author: mdeters
  ** Major contributors: barrett, dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/usage.h b/src/main/usage.h
index 9a8175e2a..6c44fef5a 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -2,7 +2,7 @@
 /** usage.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 30fb33a32..0fdde07ff 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** antlr_parser.cpp
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
- ** Minor contributors (to current version): none
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 0cdf9f36b..bfdc4c0f2 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -1,8 +1,8 @@
 /* *******************                                                        */
 /*  cvc_parser.g
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index b9e2d576e..84796f093 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -2,7 +2,7 @@
 /** parser.cpp
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 170e1af31..da2c630ca 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -2,7 +2,7 @@
 /** parser.h
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index d790a1c84..dd110c4c1 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -1,4 +1,4 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** symbol_table.h
  ** Original author: cconway
  ** Major contributors: dejan, mdeters
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 80a8819b9..5dd57610d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** prop_engine.cpp
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9aa1ecff8..d4007e73a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** prop_engine.h
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): dejan
+ ** Major contributors: taking, dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 350537d8f..a9696162a 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** sat.h
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 36954ace4..bb3e8c058 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2,7 +2,7 @@
 /** smt_engine.cpp
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): taking
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0e7e951f8..838f9cd7a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -2,7 +2,7 @@
 /** smt_engine.h
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): taking
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/theory.h b/src/theory/theory.h
index dffc99053..831a185f8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -2,7 +2,7 @@
 /** theory.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
index a22faf61e..cb7add487 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/ecdata.cpp
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** ecdata.cpp
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 #include "theory/uf/ecdata.h"
 
 using namespace CVC4;
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index fd0855bee..c8303a245 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** ecdata.h
  ** Original author: taking
- ** Major contributors: barrett
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 840c7b51e..1f4d80b9b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** theory_uf.cpp
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/ecdata.h"
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 06b0ee4f8..0ab51ca2c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** theory_uf.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 
 #ifndef __CVC4__THEORY__THEORY_UF_H
 #define __CVC4__THEORY__THEORY_UF_H
diff --git a/src/util/configuration.h b/src/util/configuration.h
index b761f1f22..20d00a5f8 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -2,7 +2,7 @@
 /** configuration.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): taking
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/options.h b/src/util/options.h
index cad00a61b..404700a85 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** options.h
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/output.h b/src/util/output.h
index ad42416d8..d0db064f0 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -2,7 +2,7 @@
 /** output.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index c145cf752..591a85202 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -51,11 +51,6 @@ EXTRA_DIST = \
 	no_cxxtest \
 	$(TEST_DEPS_DIST)
 
-# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
-noinst_LTLIBRARIES = libdummy.la
-libdummy_la_SOURCES = expr/node_black.cpp
-libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
-
 MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
 
 @mk_include@ @srcdir@/Makefile.tests
@@ -88,6 +83,13 @@ EXTRA_DIST = \
 
 endif
 
+# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
+if CVC4_FALSE
+noinst_LTLIBRARIES = libdummy.la
+libdummy_la_SOURCES = expr/node_black.cpp
+libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
+endif
+
 # synonyms for "check"
 .PHONY: regress test
 regress test: check
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index dbf434ed2..150d88306 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** parser_black.h
  ** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences