QuickChecking static analysis properties

Jan Midtgaard, Anders Møller

Research output: Contribution to journalJournal articleResearchpeer-review

217 Downloads (Pure)


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 to test 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, eg, monotone, strict, or invariant. We substantiate our claims by quickchecking a type analysis for the Lua programming language.
Original languageEnglish
Article numbere1640
JournalSoftware Testing, Verification and Reliability
Issue number6
Number of pages23
Publication statusPublished - 2017
Event8th IEEE International Conference on Software Testing, Verification, and Validation - Graz Congress, Graz, Austria
Duration: 14 Apr 201616 Apr 2016


Conference8th IEEE International Conference on Software Testing, Verification, and Validation
LocationGraz Congress


  • Domain-specific languages
  • Monotonicity
  • Quickchecking
  • Static program analysis


Dive into the research topics of 'QuickChecking static analysis properties'. Together they form a unique fingerprint.

Cite this