IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2014 > QuickChecking Static Analysis Properties
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Jan Midtgaard

jueves 11 de septiembre de 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.