Enhanced extended static checking in JML4: Benefits of multiple-prover support

The implementations of many seemingly simple algorithms are be-yond the ability of traditional Extended Static Checking (ESC) tools to verify. Not being able to verify toy examples is often enough to turn users off of the idea of using formal methods. ESC4, the ESC component of the JML4 project, is able to verify many more kinds of methods in part because of its use of novel techniques which apply multiple theorem provers. In particular, we present Offline User-Assisted ESC (OUA-ESC), a new form of verification that lies between ESC and Full Static Program Verification (FSPV), that al-lows users to control the level of completeness of the tool. ESC4’s improved performance should encourage greater use of static veri-fication