QuickChecking Static Analysis Properties

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
PublisherIEEE
Publication year2015
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
Nummer8
LandAustria
ByGraz
Periode13/04/201517/04/2015

See relations at Aarhus University Citationformats

ID: 86568291