Homework Logistics

All homework must be completed individually.

Turn in the Formal component of each assignment via Gradescope and the Coding component of each assignment via autograder.io.

You may use a tool like ChatGPT for guidance or to refine your prose. However, you are responsible for the formal correctness of all of your answers, so generative AI "hallucinations" are a very real concern. I recommend coming up with your answers on your own and then double-checking with ChatGPT or asking it to check your English prose for clarity.

You can definitely use any textbook or article. Just cite your sources in your homework (there is no specific format; just make sure I can tell which other sources you used).

You may not use an answer (or partial answer) from another human or student. For example, if you find a GitHub repository online that has answers, you may not use those (and should report that to me).

Latex Source

Latex source files for all of the homework instructions are available. These give examples for all of the special typesetting.

Homework Assignments

Homework 0 — Model Checking

Homework 0 written instructions. Resources:

• CPA Checker — The Configurable Software-Verification Platform — version 4.0 (or version 2.0 if necessary)
• tcas.i — a simplified implementation of a traffic collision avoidance system provided by Himanshu Jain
• Property1a.spc
• Property1b.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 Property1b.spc tcas.i
  3. /path/to/CPAChecker/scripts/cpa.sh -predicateAnalysis -spec Property2b.spc tcas.i

Peer Review

Download an anonymized assignment, evaluate the work of that peer, and submit your assessment via gradescope.

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 3 — Regular Expressions and SAT

Homework 3 written instructions. Resources:

• Homework 3 code.

Homework 4 — Axiomatic Semantics 1

Homework 4 written instructions. Resources:

• Answers to previous student questions.

Homework 5 — Axiomatic Semantics 2

Homework 5 written instructions. Resources:

• Answers to previous student questions.

Homework 6 — Test Input Generation

Homework 6 written instructions. Resources:

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

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