ESC can be thought of as an extended form of type checking. […] it promotes practicality over soundness, in that it aims to dramatically reduce the number of false positives (overestimated errors that are not real errors, that is, ESC over strictness) at the cost of introducing some false negatives (real ESC underestimation error, but that need no programmer’s attention, or are not targeted by ESC). ESC can identify a range of errors which are currently outside the scope of a type checker, including division by zero, array out of bounds, integer overflow and null dereferences.
Extended static checking achieves “Absence of RunTime Exceptions” (AoRTE) which is things like
- No division by zero
- No integer overflow
- Memory safety
- All array accesses in bounds
- No null dereferences
- No buffer overflows
- No use after free
- No memory leaks
- Lock safety of concurrent code
The nice thing about extended static checking is that you don’t have to write specifications or proofs.
The software verification competition SV-COMP mostly checks properties like this.
Notes related to Extended static checking (ESC)
Papers related to Extended static checking (ESC)
- CPAchecker: A tool for configurable software verification [beyer:cav:2011]
- The software model checker BLAST: Applications to software engineering [beyer:ijsttt:2007]
- Extended static checking: A ten-year perspective [leino:informatics:2001]
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
- Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]