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 language | English |
|---|---|
| Title of host publication | Proceedings of th 8th International Conference on Software Testing, Verification, and Validation (ICST 2015) |
| Publisher | IEEE |
| Publication date | 2015 |
| Pages | 1-10 |
| ISBN (Print) | 978-1-4799-7125-1 |
| Publication status | Published - 2015 |
| Externally published | Yes |
| Event | 8th International Conference on Software Testing, Verification, and Validation (ICST 2015) - Graz, Austria Duration: 13 Apr 2015 → 17 Apr 2015 Conference number: 8 http://icst2015.ist.tu-graz.ac.at/ |
Conference
| Conference | 8th International Conference on Software Testing, Verification, and Validation (ICST 2015) |
|---|---|
| Number | 8 |
| Country/Territory | Austria |
| City | Graz |
| Period | 13/04/2015 → 17/04/2015 |
| Internet address |