SMT: bitvectors and arrays by bit-blasting. Bitme: the model of week 10 unrolled and handed to the solver of week 11 — and your own extension checked.
Satisfiability modulo theories. A propositional skeleton whose atoms are statements in a theory: bitvectors, with the machine's operations on fixed-width words; arrays, with read and write on an indexed store. SMT-LIB is the notation; Z3 and Bitwuzla read it, and BTOR2 too.
Bit-blasting. A 64-bit word is sixty-four variables; an addition is the adder circuit; every gate is three or four clauses with a fresh variable (Tseitin). Arrays get their axioms on demand. The SMT formula becomes a SAT formula, much bigger, and CDCL runs on it. Cook's construction, as engineering.
Bitme walks the steps and, at each, asks the solver about every bad state. Seventy-five steps of no while the program sets up its stack and calls malloc and read. Then, at step 76, yes, and the assignment of the input buffer is the failing input. Nobody told it to try '0'.
The step numbers move with the versions of the tools; check before class. The shape does not: a bad state, a step, an input. The same run on your own extensions is the assignment.
One input per run. Shows presence. The grader's few hundred programs are a few hundred points in the space of week 2 of the introduction class.
Every input, every path, up to k steps. Shows absence, within the bound, as a theorem. Pays in solver time that grows with k, and says nothing beyond it.
Rice forbade deciding whether a program divides by zero. This decides whether it does so within k steps — a question about a finite object. Choosing k is choosing what to give up: the sound-but-incomplete corner of week 9's table, with the incompleteness made explicit as a number.
Everything in the workshop around selfie is such a choice: rotor and bitme within a bound, the type checker for one property, buzzr complete about the crashes it happens to see. Each stated. Each applied to selfie itself.
The other half of the capstone: field access p->f as a load or store at the pointer plus the field's offset. Then use a struct in selfie.c, for the symbol table if you dare, and self-compile.
Rules as always. For rotor-check the submission is a directory with the program and a one-page note.
Strauss · Elektra — Solti, Nilsson, Vienna 1967. One act, no interruption, one question asked of every state: is it him? The recognition scene is the satisfying assignment found; the dance is what happens when the bound is reached.
Handbook of Model Checking — Clarke, Henzinger, Veith and Bloem, editors, 2018: where the field defines its terms; bounded model checking is one chapter. And, more technical, A Tool for Checking ANSI-C Programs — Clarke, Kroening and Lerda, 2004: CBMC, the bounded model checker for C that rotor and bitme are cousins of.