2012: Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata

(for 2002) Extended Static Checking for Java


This paper marks a turning point in the field of static checking, describing pragmatic design decisions that promote practicality over completeness. Pioneered in ESC/Modula-3, techniques from ESC/Java are now widely used in various forms in Microsoft’s development tools, notably as part of Code Contracts which ships with VisualStudio. Recent innovations strongly influenced by ESC/Java include refinement types for Haskell, and verification of Eiffel programs.