Tabster - A Tabular Expression Toolbox

Tables are widely used in safety-critical and embedded systems development to specify what outputs a system should produce for different classes of inputs, but tooling support for verifying their correctness has historically been limited. Tabster is a Java library that fills this gap by formally verifying properties of tabular expressions using SMT solvers. When a property fails to hold, Tabster does not just report a failure — it returns counterexamples that identify the exact input conditions under which the property breaks. This post walks through the design of the library, the kinds of properties it can verify, and how SMT solving makes exhaustive verification practical for real-world table sizes.