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 pen-and-paper soundness proofs, to verified fixed point checking. In this paper we demonstrate how quickchecking can be useful for testing a range of static analysis properties with limited effort. We show how to check a range of algebraic lattice properties, to help ensure that an implementation follows the formal specification of a lattice. Moreover, we offer a number of generic, type-safe combinators to check transfer functions and operators on lattices, to help ensure that these are, e.g., monotone, strict, or invariant. We substantiate our claims by quickchecking a type analysis for the Lua programming language.
|Title of host publication||Proceedings of th 8th International Conference on Software Testing, Verification, and Validation (ICST 2015)|
|Publication status||Published - 2015|
|Event||8th International Conference on Software Testing, Verification, and Validation (ICST 2015) - Graz, Austria|
Duration: 13 Apr 2015 → 17 Apr 2015
Conference number: 8
|Conference||8th International Conference on Software Testing, Verification, and Validation (ICST 2015)|
|Period||13/04/2015 → 17/04/2015|