IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2014 > QuickChecking Static Analysis Properties

Jan Midtgaard

Thursday, September 11, 2014

11:00am Meeting room 302 (Mountain View), level 3

Jan Midtgaard, Post-doctoral Researcher, Aarhus University, Denmark

QuickChecking Static Analysis Properties

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 soundness proofs by hand, to automated fixed point checking.

We demonstrate how quickchecking can be used to test a range of static analysis properties with limited effort. Our approach is twofold:

  • we show how we can check a range of algebraic lattice properties — to help ensure that an implementation follows the formal specification of a lattice, and

  • we offer a number of generic, type-safe combinators to check transfer functions and operators between lattices — to help ensure that these are, e.g., monotone, strict, or invariant.

We substantiate our claims by quickchecking a non-trivial type analysis for the Lua programming language.