Lessons

Each lesson runs one program past ESBMC and shows what came back, including what the front end encoded before the solver saw it. Work through a part in order; each lesson assumes the one before it.

Getting started

Small synthetic ladders, one idea each. Every program here is a few elements long, so the encoding ESBMC produces is short enough to read line by line.

lesson	what it shows
1.1 One rung: contacts and a coil	The smallest ladder that verifies. Three contacts in series, one coil, one property, one proof.
1.2 Series, parallel, and the wired OR	Two branches into one coil. The shipped property is proved, and it would have been proved just as soundly by a front end that dropped the second branch. A second property makes the branch's survival checkable.
1.3 A reversing starter, proved and broken	One motor, two contactors, one property. A k-induction proof, then the same ladder with a contact deleted and the counterexample that follows.
1.4 A seal-in latch, where the verdict hides the encoding	The circuit verifies as safe, and that verdict is equally true of a latch, of a plain conjunction, and of a program that assigns nothing. It takes a second property to tell them apart.
1.5 Edges, and the order rungs run in	Three rungs whose order is the design. Both builds run them in an order the file never specified, and the standard says the benchmark is right.
1.6 Timers, and the tick they count	A preset is measured in scans. One build models the timer, the other drops the block, and the benchmark's own property turns out to be false of an off-delay.
1.7 Counters, and a pin that is not read	CTU counts and resets. CTD wires its IEC load pin, the front end reads only R, and the modelled counter never reloads.
1.8 Memory and time together	A timer sets a latched alarm and an acknowledgement clears it. Reset dominance is correct here, and the reason it is correct is an accident of emission order.

Machines and their hazards

Real plants, one industrial domain at a time. Each lesson names the machine, the thing that must never happen to it, and what a verifier does with a program in which someone hid a way to make it happen.

lesson	what it shows
2.1 A conveyor that ignores its emergency stop	One added branch, conducting only when the E-stop is pressed and a maintenance key is turned, and the counterexample that hands you the combination.
2.2 A reactor that keeps feeding under pressure	The same bypass in a chemical plant, where the relief vent still works and makes the attack look like a functioning protection system. Then a reasonable-sounding weakening of the property that lets the bomb through.
2.3 A junction that shows two greens	The bypass a third time, and a careful account of what conflict-freedom leaves open: no intergreen, no minimum green, and a stuck detector that starves one arm forever.
2.4 A car that moves with its door open	The same machine as a rung and as a chart. One bomb adds a branch, the other changes a single letter, and only one of them is caught.
2.5 An air handler whose name promises a timer	Heating and cooling interlocked correctly, a bypass that defeats it, and a benchmark called fan_delay whose program contains no block at all.
2.6 A substation, three interlocks and one key	Busbar, breaker and transformer defeated by the same input, and the protection layer the attacker deliberately leaves working.
2.7 The override you cannot tell from the attack	The same branch is a legitimate maintenance override or a bomb, and nothing in the program decides which. The property does.
2.8 The family, and what it does not cover	All twelve machines in one table, what is identical and what changes across them, and the trigger shapes this part never showed.

Logic-level bombs

The same programs, organized by the shape of the attack rather than by the plant it was fitted to, and the trigger shapes that defeat testing by construction.

lesson	what it shows
3.1 What a logic-level bomb is	Trigger, payload and dormancy, the three trigger shapes the catalog carries, and why sampling cannot find any of them.
3.2 Bombs that wait	A fifty-scan fuse, SAFE at eight scans and VIOLATION at sixty-four, and why the first answer is a correct proof about the wrong program.
3.3 When the fuse outruns the checker	Five identical bombs at fuse widths from 255 to 32767 scans, all found, at 0.9 seconds and 406 seconds respectively, and why unwinding further is a race the defender loses.
3.4 The payload that produces no output	A loop whose counter is never advanced, entered at one sensor value, and the scan watchdog that catches it. Plus the flag combination that reports the hang as proved.
3.5 The counterexample as the recovered knock	A reachability property inverted into an assertion, unreachable on the clean program and recovering fwd, rev and maint on the bombed one, which is exactly what was planted.
3.6 What a property has to say	Eight things the failures on this site have in common, from naming a consequence to carrying the bound, and the twenty-six recorded runs whose verdict meant nothing.

Code from the plant

Programs neither of us wrote: what a real engineering tool emits, and what it costs to verify code that arrived from somewhere else.

lesson	what it shows
4.1 The one file nobody here wrote	A 2019 TwinCAT export: the only program of fifty-five that passed the PLCopen schema, and the one where nothing is where the standard says it should be.
4.2 What real plant code costs	Five SWaT benchmarks that cannot be ported without deleting the bomb, because the attack is written in a vendor exception mechanism. The sixth now has a verdict, once termination stopped being treated as inexpressible.

Bombs from a public dataset

Eight legitimate and malicious pairs of one water tank controller, published by other people with their own labels, and a single property that refutes all eight.

lesson	what it shows
5.1 A tank, and eight ways to stop it	The plant, the one property that covers every attack in this part, and why a program that never finishes a scan is worse than one that computes the wrong answer.
5.2 The loop that never ends	Ten lines appended to a working function block, a counter assigned on every pass that never advances, and a trigger whose constant is not the sensor value that fires it.
5.3 A block that is not the block it names	EQ becomes EQ_0, the replacement reimplements equality correctly, and the payload sits below the part that answers the question a reviewer came with.
5.4 The refactor that carried a payload	A POU deleted and its logic inlined, which is a large diff with a plausible story attached, and the one attack that names the raw input in its guard.
5.5 Eight bombs, one property	Sixteen programs settled in 0.74 seconds, and what termination covers that an interlock property cannot.

The languages ladder cannot reach

Function block diagrams and sequential function charts, where the ladder front end reads nothing and says so in three different ways: a missed defect, a false alarm, and a proof about an empty program.

lesson	what it shows
6.1 A diagram the checker never read	An air handler permissive with one wire deleted. The ladder route now refuses the file by name, which it did not do until esbmc#7354 was fixed, and the C route names the violated property.
6.2 The false alarm	A two-out-of-three vote that works, once refuted with a plausible counterexample and now refused outright. The table that made the case for recording encodings, and why the fix does not retire it.
6.3 Four charts and no verdict	Every SFC benchmark is refused at parse, which is an improvement on the SAFE they used to report. Pointing the second route at them broke in three different layers, and the third has not been cleared.
6.4 The spelling nothing here reads	Ladder written as text rather than drawn. Fifteen programs, no recorded run on either route, and twelve graphical twins that verify while the files beside them cannot be checked at all.

Safety functions from the standards

Seven machines whose control logic exists because a clause in a standard asks for it. Each one ships the property an engineer would write, a second program the property cannot tell apart from the first, and the property that can.

lesson	what it shows
7.1 The reset nobody has to press	A monitored reset and an automatic restart, and one emergency-stop property that is true of both. The discriminator is refuted in the first scan, which is the requirement arriving on time.
7.2 Both buttons held, and the press stays up	ISO 13851 Type II against Type I. The obvious property is true of the device you can defeat with tape, and true of it for a stronger reason than of the good one.
7.3 The gap between two contactors	Mutual exclusion proved on a starter with a dead time and on one without. What the proof covers is two program variables, and a contactor is not a program variable.
7.4 The door that pauses instead of reversing	A latched reversal and a momentary one. The safety property is true of both; only a question about what the latch still holds after the beam clears tells them apart.
7.5 A lockout that lets go	EN 298 light-off order, proved on a burner whose lockout clears itself. The order is right in both programs, and only the lockout question separates them.
7.6 The standby pump nobody started	Duty-standby alternation, and the first discriminator in this part that neither build can discharge. A five-line reproducer of a k-induction limit comes with it.
7.7 The guard that waits for the spindle	ISO 14119 guard locking with a real rundown timer. The discriminator asks whether the program waits rather than whether it remembers.
7.8 The interlock that makes it wait	A minimum-off interlock against a short-cycling twin, and the table that has been the same in every discriminator pair.
7.9 The block the checker stops reading	Lesson 7.2's press moved into a function block. Both builds fail the gate on the correct program and refute a property that holds on the correct variant, because block parameters are never bound and a boolean body loses an operand.
7.10 Two textbook rungs, transcribed	A cross-interlocked forward/reverse starter that stays safe in a scan cycle because rungs run in drawing order, a translator artifact that once said otherwise, and a fail-safe latch whose textbook property will not parse until an implication is rewritten by hand.