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
     • 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).
   • Instructions for getting BLAST working on a Mac.

   • "Answer Key" to the Set Theory Problem
1. Homework 1 Written
   Homework 1 Code.
2. Homework 2 Written
   Homework 2 Code.
   • "Answer Key" to "Try"
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}.
   • "Answer Key" to Regular Expressions
4. Homework 4 Written
   • Answers to student questions.
   • "Answer Key" to Homework 4
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 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)

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.

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.