kirancodes.me
To Proof Maintenance & Beyond!

Testing static analyses for precision and soundness

Jubi Taneja, Zhengyang Liu, John Regehr

Abstract

Static analyses compute properties of programs that are true in all executions, and compilers use these properties to justify optimizations such as dead code elimination. Each static analysis in a compiler should be as precise as possible while remaining sound and being sufficiently fast. Unsound static analyses typically lead to miscompilations, whereas imprecisions typically lead to missed optimizations. Neither kind of bug is easy to track down.

Related papers