September 11, 2014
Jan Midtgaard
A static analysis can check programs for potential errors. A natural question that arises is therefore: who checks the checker? Researchers have given this question varying attention, ranging from basic testing techniques, informal monotonicity arguments, thorough soundness proofs by hand, to automated fixed point checking.
We demonstrate how quickchecking can be used to test a range of static analysis properties with limited effort. Our approach is twofold:
-
we show how we can check a range of algebraic lattice properties — to help ensure that an implementation follows the formal specification of a lattice, and
-
we offer a number of generic, type-safe combinators to check transfer functions and operators between lattices — to help ensure that these are, e.g., monotone, strict, or invariant.
We substantiate our claims by quickchecking a non-trivial type analysis for the Lua programming language.