Rotor turns a program into a formula. Bitme asks a solver whether any input reaches a bad state within a bound.
Registers and memory are bit-vectors. Each of the fourteen instructions is a function from state to state. A program's semantics, from the Meaning chapter, is exactly the transition relation of a BTOR2 model: init, next, and a list of bad states.
Unroll next k times, conjoin one bad state, hand the formula to an SMT solver. Satisfiable: an input reaches the bad state at step k, and the assignment is that input. Unsatisfiable up to a bound: no input reaches it within the bound, a theorem.
Rotor is selfie's model generator. It compiles the program, then emits the machine as a formula: registers, memory segments, the fourteen instructions, and the system calls as what the kernel does to the state. Input bytes are the free variables.
The bad states are systems properties: an address outside the mapped segments, a fetch from data, a store into code, a break that moves backwards, a non-zero exit. Memory safety, as formulas over the state the kernel manages.
Step by step, every bad state is asked. Seventy-five steps of no while the program sets up its stack and calls read. Then, at step 76, where the division is fetched, yes, and the solver hands back the byte that gets there: the character zero. A failing input, derived, not guessed. Step numbers and format move with the tools; the shape does not. Check before class.
The same run on a segmentation fault looks identical, with a different bad state and an input that computes a bad address. That is the point for a systems engineer: the exceptions your kernel handles are the properties the model checker searches for, and the search is exhaustive up to the bound.
A test visits one state in a space of 235 bits per machine. A bounded run covers every input and every path to depth k. Presence versus absence; observation versus theorem.
No tool decides whether a program segfaults. This one decides whether it does within k steps, which is a different, finite question. The bound is the approximation, chosen and named, like the timer and the TCB.
Rotor models one machine context. Interleavings, week 8's state space, are not in the formula. Modelling them is a research problem with real tools, and not this class's. The formal-methods assignment stays sequential, and says so.
The grader runs rotor and bitme on your driver and compares verdict and bound; the invocation is in the assignment file. Two weeks for both. The stack is the harder code; the model is the harder thinking.
Bach · Canonic Variations on “Vom Himmel hoch” — Robert Costin, organ. One hymn, five canons at fixed intervals, each checked strictly against the rule while the tune runs through unchanged; the last inverts and augments at once. A property, a bound and a model, in 1747.
Decision Procedures: An Algorithmic Point of View — Kroening and Strichman: the textbook on SMT, bit-vectors, arrays and bit-blasting, written for exactly the purpose of checking programs. And, more technical, Symbolic Model Checking without BDDs — Biere, Cimatti, Clarke and Zhu, 1999: bounded model checking, the k that bitme runs, in the paper that invented it.