Extended static checking: Difference between revisions

Revision as of 14:07, 21 January 2022

Revision as of 14:13, 21 January 2022

Line 1:

'''Extended static checking''' ('''ESC''') is a collective name in [[computer science]] for a range of techniques for [[static code analysis|statically checking]] the correctness of various program constraints.<ref>C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, [[James B. Saxe|J. B. Saxe]] and R. Stata. "Extended static checking for Java". In ''Proceedings of the Conference on Programming Language Design and Implementation'', pages 234-245, 2002. doi: http://doi.acm.org/10.1145/512529.512558</ref> ESC can be thought of as an extended form of [[type checking]]. As with type checking, ESC is performed automatically at [[compile time]] (i.e. without human intervention). This distinguishes it from more general approaches to the [[formal verification]] of software, which typically rely on human-generated proofs. Furthermore, 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).<ref name=GNESCUWCSC /><ref>{{cite conference | last=Babic | first=Domagoj | last2=Hu | first2=Alan J. | title=Calysto: Scalable and Precise Extended Static Checking, Domagoj| Babicpublisher=ACM andPress Alan J. Hu. In| conference=Proceedings of the International Conference on Software Engineering (ICSE),| year=2008. {{DOI| doi=10.1145/1368088.1368118 | page=}}</ref> ESC can identify a range of errors which are currently outside the scope of a type checker, including [[division by zero]], [[bounds checking|array out of bounds]], [[integer overflow]] and [[Null pointer|null dereferences]].

The techniques used in extended static checking come from various fields of computer science, including [[static program analysis]], [[symbolic simulation]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]] and [[type checking]]. Extended static checking is generally performed only at an intraprocedural level (rather than an interprocedural one) in order to scale to large programs.<ref name=GNESCUWCSC>{{Cite web