Homework Assignments

Do not make use of any other delivery method for your homework (e.g., carrier pigeons, my faculty mailbox).

Homeworks:

0. Homework 0 Written
   • BLAST Project
   • BLAST Manual
   • tcas.i testcase -- TCAS is an implementation of a traffic collision avoidance system provided by Himanshu Jain.
   • Commands:
     1. pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY1A
     2. pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY2B
   • Instructions for getting BLAST working on a Mac.
1. Homework 1 Written
   Homework 1 Code.
2. Homework 2 Written
   Homework 2 Code.
3. Homework 3 Written
   • Liskov et al. paper
   • Stroustrup paper
   Homework 3 Code.
   [\![\,Exp\,]\!] is a reasonable LaTeX command for [[Exp]]. You might also make a macro like this: \newcommand{\sem}[1]{[\![\,#1\,]\!]} and then use \sem{Exp}.
4. Homework 4 Written
   • Answers to student questions.
5. Homework 5.
   1. Homework 5 Written
   2. Homework 5 Code.
   3. Download one of the versions of Simplify below and rename it to $TOP/Simplify (i.e., put it in the same directory as nf.ml).
      • Simplify (for Windows) or
      • Simplify (for Linux) or
      • Simplify (for OS X) or
      • Simplify (for Solaris)
   4. Necula et al.'s CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs (optional)
   5. Detlefs, Nelson and Saxe's Simplify: A Theorem Prover For Program Checking (optional, huge PDF)
   6. Manuvir Das' Unification-based pointer analysis with directional assignments (optional, the GOLF paper)
   7. Bush, Pincus and Seilaff's A Static Analyzer For finding Dynamic Programming Errors (optional, the PREfix paper)
   8. The CIL Manual. In particular, check out the CIL API Documentation (or read cil/src/cil.mli). (optional)
   9. O'Reilly's Developing Applications With Objective Caml (really optional, but if you feel you need extra help with OCaml, this book probably has the answers -- you can also talk to me)
   10. Precompiled x86 CYGWIN version of the Homework 5 code. Use this if you can't get CIL to build yourself; typically that's indicative of other problems, however.

The list of tortured bits of English prose remains available.

Calls For Papers, Fun Venues, Internships, Summer Activities

• Every Thursday the Theory Lunch convenes. Free food is provided and we occasionally even discuss theory. The setting is quite informal, with an emphasis on good ideas and fun rather than being stuffy.
• The Security Reading Group convenes weekly.

Random Somewhat-Related Humor

1. Research Glossary (note "interesting to me")
2. The Guru of Chelm (evaluating systems)
3. How To Prove It (alternative techniques to structural induction)
4. K-Coward (taking math too seriously)
5. Hamlet PowerPoint (problems with all-PowerPoint presentations)
6. Universal Poker (proof theory: why is Truth's opposite "Void"?)
7. Chess Books (useful background reading)
8. Polynomial Hierarchy Collapses: Thousands Feared Tractable
9. Microsoft Patches (exceptional situations and error handling)
10. C Problem (essential debugging)
11. USENET Homework (asking for help)
12. Linux Development Order (requirements engineering)
13. GCC International (promoting international understanding)
14. Microsoft Buys TeX (note "What were we thinking?" and "third-party display driver")
15. Feel-Good Abstraction (at what level should we analyze and design?)
16. Parametric Worm (Microsoft security explained)
17. 1776 Computers (historical perspectives)
18. Security Important (system and user security)
19. Secure README (security through obscurity)
20. Tarzan Learns Email (explaining CS to the laity)
21. Jobs Translated (meanings of terse utterances)
22. How I Met My Wife (is Wes speaking English?)

Other Similar Courses

• Cornell CS 611 2005 Homework #1.
• Washington CSE 505 2005 Homework #1.