QuickChecking Static Analysis Properties

Jan Midtgaard, Anders Møller

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review


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
Original languageEnglish
Title of host publication 8th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2015
Number of pages10
Publication date2015
Publication statusPublished - 2015
EventInternational Conference on Software Testing, Verification and Validation - Graz, Austria
Duration: 13 Apr 201517 Apr 2015
Conference number: 8


ConferenceInternational Conference on Software Testing, Verification and Validation

Cite this