QuickChecking Static Analysis Properties

Jan Midtgaard, Anders Møller

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

Abstract

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
PublisherIEEE
Publication date2015
Pages1-10
DOIs
Publication statusPublished - 2015
EventInternational Conference on Software Testing, Verification and Validation - Graz, Austria
Duration: 13 Apr 201517 Apr 2015
Conference number: 8

Conference

ConferenceInternational Conference on Software Testing, Verification and Validation
Number8
Country/TerritoryAustria
CityGraz
Period13/04/201517/04/2015

Cite this