Homework Logistics

All homework must be completed individually on in pairs (your choice).

Turn in each assignment via the UM Canvas system.

Homework 0 — Model Checking

Homework 0 written instructions. Resources:

• CPA Checker — The Configurable Software-Verification Platform — version 1.6.1
• tcas.i — a simplified implementation of a traffic collision avoidance system provided by Himanshu Jain
• Property1a.spc
• Property2b.spc
• Example commands:
  1. /path/to/CPAChecker/scripts/cpa.sh -predicateAnalysis -spec Property1a.spc tcas.i
  2. /path/to/CPAChecker/scripts/cpa.sh -predicateAnalysis -spec Property2b.spc tcas.i

Homework 1 — Basic Operational Semantics

Homework 1 written instructions. Resources:

• Homework 1 code.

Homework 2 — Induction and Imperative Features

Homework 2 written instructions. Resources:

• Homework 2 code.
• Homework 2 LaTeX source and LaTeX Style File.
• Partial Answer Key

Homework 3 — Regular Expressions and SAT

Homework 3 written instructions. Resources:

• Homework 3 code.
• Homework 3 LaTeX source.
• Partial Answer Key (also includes denotational semantics material not relevant for this year)

Homework 4 — Axiomatic Semantics

Homework 4 written instructions. Resources:

• Homework 4 LaTeX source.
• Answers to previous student questions.
• Partial Answer Key

Homework 5 — Test Input Generation

Homework 5 written instructions. Resources:

• 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)

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?)