QuickChecking Static Analysis Properties

Jan Midtgaard, Anders Møller

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer 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
OriginalsprogEngelsk
Titel 8th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2015
Antal sider10
ForlagIEEE
Publikationsdato2015
Sider1-10
DOI
StatusUdgivet - 2015
BegivenhedInternational Conference on Software Testing, Verification and Validation - Graz, Østrig
Varighed: 13 apr. 201517 apr. 2015
Konferencens nummer: 8

Konference

KonferenceInternational Conference on Software Testing, Verification and Validation
Nummer8
Land/OmrådeØstrig
ByGraz
Periode13/04/201517/04/2015

Emneord

  • Computer languages
  • DSL
  • Generators
  • Lattices
  • Resource management
  • Testing
  • Transfer functions

Citationsformater