Benjamin Bürki
M.Sc. thesis in Cyber
June 23, 2026
Abstract:
This project is situated in formal verification and studies how Grounded
Deduction can be used to reason about recursive, trace-producing computations.
The focus is a small HRM-style machine whose processor, input device, and
output device are defined by mutually recursive functions and whose execution
produces observable event traces.
The main difficulty is that before proving safety or liveness of such traces,
we must first justify that the recursively defined execution actually produces
a well-defined object. Classical verification frameworks can reason about
program correctness, but definedness, termination, and trace-level behaviour
are often handled as separate proof obligations or encoded indirectly.
The high-level idea of this work is to use the GD principle of habeas quid:
before using a computed object in a proof, we first prove that it is grounded.
The verification is therefore organized in layers: first prove that finite
observations of execution produce grounded finite traces, then reason about
safety and liveness on those traces.
A key design decision is to make execution produce explicit events. The
processor delegates input and output actions to separate device functions,
which append their own events to the trace and return control through
first-order continuation tags. This keeps the model recursive and modular while
making the observable behaviour explicit.
The evaluation shows that the design supports the intended proof pattern.
Finite executions yield grounded finite traces, trace-processing functions
terminate on finite traces, and finite safety is a grounded predicate. Infinite
safety is obtained by checking all finite prefixes, while liveness is stated on
infinite traces and inherited by finite traces through prefix reasoning.