Homework Assignments

Homework is due at 11:50 pm on the day indicated unless otherwise noted.

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
     • Be sure to get BLAST 2.5 — older versions will not work.
   • BLAST Manual
   • tcas.i testcase -- TCAS is an implementation of a traffic collision avoidance system provided by Himanshu Jain.
   • Commands:
     1. export PATH=.:$PATH
     2. pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY1A
     3. pblast.opt -craig 2 -dfs -nolattice tcas.i -L PROPERTY2B
   • Note that BLAST often writes the counter-example trace to a file in the current directory (and not to the screen).
   • BLAST may not work on a modern OSX Mac. If so, you'll have to find a working machine (e.g., department Unix machine, Unix VM image, etc.). Old instructions for getting BLAST working on a Mac are available but may not work for you. The instructor does not provide support for running BLAST on a Mac.
1. Homework 1 Written
   Homework 1 Code.
2. Homework 2 Written
   Homework 2 Code.
   Homework 2 LaTeX Source and Homework LaTeX Style File.
   Homework 2 Partial Answer Key.
3. Homework 3 Written
   Homework 3 Code.
   Homework 3 LaTeX Source.
   Homework 3 Partial Answer Key (includes extra denotational semantics information not relevant for this year's course).
4. Homework 4 Written
   Homework 4 LaTeX Source
   • Answers to student questions.
   Homework 4 Complete and Detailed Answer Key.
5. Homework 5.
   • Homework 5 Written
   • Homework 5 Code.
   • Parsing and Analyzing C Programs
     • Necula et al.'s CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs (optional)
     • Zachary Anderson's CIL Tutorial (includes worked code snippets and examples)
     • The CIL Manual. In particular, check out the CIL API Documentation (or read cil/src/cil.mli). (optional)
   • Automated Theorem Proving
     • de Moura and Bjorner's Z3: An Efficient SMT Solver (optional)
     • The Z3 Webpage. In particular, check out the Z3 OCaml API Documentation. (optional)
   • Automated Test Input Generation
     • Godefroid, Klarlund and Sen's DART: directed automated random testing. (optional)
     • Sen, Marinov and Agha's CUTE: a concolic unit testing engine for C (optional)
     • Xie, Marinov, Schulte and Notkin's Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (optional)
     • Lakhotia, McMinn and Harman's An empirical investigation into branch coverage for C programs using CUTE and AUSTIN (optional)
     • Tillmann and de Halleux's Pex — White Box Test Generation for .NET (optional)
     • The Pex Project (Pex for Fun) (optional, fun)
     • The AUSTIN Project (optional)
     • The CREST Project (optional)
   • Alias Analysis
     • Manuvir Das' Unification-based pointer analysis with directional assignments (optional)
   • String Analysis
     • Hooimeijer and Weimer's A Decision Procedure for Subset Constraints over Regular Languages (optional)
     • The DPrle Project (optional)

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.