Extended static checking: Difference between revisions
Cybercobra (talk | contribs) mNo edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
'''Extended Static Checking (ESC)''' is a collective name 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, 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 system#Type checking|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 completeness, in that it aims to dramatically reduce the number of ''false positives'' (reported errors that are, in fact, not errors) at the cost of introducing some ''false negatives'' (real errors which are not reported)<ref>Calysto: Scalable and Precise Extended Static Checking, Domagoj Babic and Alan J. Hu. In Proceedings of the International Conference on Software Engineering (ICSE), 2008. doi: http://dx.doi.org/10.1145/1368088.1368118</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 [[pointer (computing)#Null pointer|null dereferences]]. |
'''Extended Static Checking (ESC)''' is a collective name 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, 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 system#Type checking|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 completeness, in that it aims to dramatically reduce the number of ''false positives'' (reported errors that are, in fact, not errors) at the cost of introducing some ''false negatives'' (real errors which are not reported)<ref>Calysto: Scalable and Precise Extended Static Checking, Domagoj Babic and Alan J. Hu. In Proceedings of the International Conference on Software Engineering (ICSE), 2008. doi: http://dx.doi.org/10.1145/1368088.1368118</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 [[pointer (computing)#Null pointer|null dereferences]]. |
||
The techniques used in extended static checking come from various fields of [[Computer Science]], including [[static analysis]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]]. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an |
The techniques used in extended static checking come from various fields of [[Computer Science]], including [[static analysis]], [[model checking]], [[abstract interpretation]], [[satisfiability modulo theories|SAT solving]] and [[automated theorem proving]]. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an interprocedural one). Furthermore, it aims to report errors by exploiting user-supplied specifications, in the form of [[precondition|pre-]] and [[postcondition|post-conditions]], [[loop invariant|loop invariants]] and [[class invariant|class invariants]]. |
||
Extended static checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strongest postconditions]] (resp. [[predicate transformer semantics#Weakest preconditions|weakest preconditions]]) intraprocedurally through a method starting from the precondition (resp. postcondition). At each point during this process an intermediate condition is generated that captures what is known at that program point. This is combined with the necessary conditions of the program statement at that point to form a ''verification condition''. An example of this is a statement involving a division, whose necessary condition is that the [[divisor]] be non-zero. The verification condition arising from this effectively states: ''given the intermediate condition at this point, it must follow that the divisor is non-zero''. All verification conditions must be shown correct in order for a method to pass extended static checking. Typically, some form of automated theorem prover is used to discharge verification conditions. |
Extended static checkers typically operate by propagating [[predicate transformer semantics#Strongest postcondition|strongest postconditions]] (resp. [[predicate transformer semantics#Weakest preconditions|weakest preconditions]]) intraprocedurally through a method starting from the precondition (resp. postcondition). At each point during this process an intermediate condition is generated that captures what is known at that program point. This is combined with the necessary conditions of the program statement at that point to form a ''verification condition''. An example of this is a statement involving a division, whose necessary condition is that the [[divisor]] be non-zero. The verification condition arising from this effectively states: ''given the intermediate condition at this point, it must follow that the divisor is non-zero''. All verification conditions must be shown correct in order for a method to pass extended static checking. Typically, some form of automated theorem prover is used to discharge verification conditions. |
||
Revision as of 12:11, 21 December 2010
Extended Static Checking (ESC) is a collective name for a range of techniques for statically checking the correctness of various program constraints[1]. 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 completeness, in that it aims to dramatically reduce the number of false positives (reported errors that are, in fact, not errors) at the cost of introducing some false negatives (real errors which are not reported)[2]. 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.
The techniques used in extended static checking come from various fields of Computer Science, including static analysis, model checking, abstract interpretation, SAT solving and automated theorem proving. One characteristic is that ESC is generally performed only at an intraprocedural level (rather than an interprocedural one). Furthermore, it aims to report errors by exploiting user-supplied specifications, in the form of pre- and post-conditions, loop invariants and class invariants.
Extended static checkers typically operate by propagating strongest postconditions (resp. weakest preconditions) intraprocedurally through a method starting from the precondition (resp. postcondition). At each point during this process an intermediate condition is generated that captures what is known at that program point. This is combined with the necessary conditions of the program statement at that point to form a verification condition. An example of this is a statement involving a division, whose necessary condition is that the divisor be non-zero. The verification condition arising from this effectively states: given the intermediate condition at this point, it must follow that the divisor is non-zero. All verification conditions must be shown correct in order for a method to pass extended static checking. Typically, some form of automated theorem prover is used to discharge verification conditions.
Extended Static Checking was pioneered in ESC/Modula-3[3] and, later, ESC/Java. Its roots originate from more simplistic static checking techniques, such as used in Lint (software) and FindBugs. A number of other languages have adopted ESC, including Spec# and SPARKada. However, there is currently no widely used programming language that provides extended static checking.
References
- ^ C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, 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
- ^ Calysto: Scalable and Precise Extended Static Checking, Domagoj Babic and Alan J. Hu. In Proceedings of the International Conference on Software Engineering (ICSE), 2008. doi: http://dx.doi.org/10.1145/1368088.1368118
- ^ An extended Static Checker for Modula-3, K. Rustan M. Leino and Greg Nelson. In Proceedings of the Conference on Compiler Construction, pages 302--305, 1998. doi: http://dx.doi.org/10.1007/BFb0026418
Further reading
- Flanagan, Cormac; Leino, K. Rustan M.; Lillibridge, Mark; Nelson, Greg; Saxe, James B.; Stata, Raymie (2002). "Extended static checking for Java". Proceedings of the Conference on Programming Language Design and Implementation (PLDI): 234. doi:10.1145/512529.512558.
{{cite journal}}: More than one of|first1=and|first=specified (help); More than one of|last1=and|last=specified (help); Unknown parameter|coauthors=ignored (|author=suggested) (help) - Babic, Domagoj; Hu, Alan J. (2008). "Calysto: Scalable and Precise Extended Static Checking". Proceedings of the International Conference on Software Engineering (ICSE): 211. doi:10.1145/1368088.1368118.
- Chess, B.V. (2002). "Improving computer security using extended static checking". Proceedings of IEEE Symposium on Security and Privacy: 160–173. doi:10.1109/SECPRI.2002.1004369.
- Rioux, Frédéric; Chalin, Patrice (2006). "Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study". Electronic Notes in Theoretical Computer Science. 157 (2): 119–132. doi:10.1016/j.entcs.2005.12.050. ISSN 1571-0661.
- James, Perry R.; Chalin, Patrice (2009). "Faster and More Complete Extended Static Checking for the Java Modeling Language". Journal of Automated Reasoning. 44 (1–2): 145–174. doi:10.1007/s10817-009-9134-9. ISSN 0168-7433.
- Xu, Dana N. (2006). "Extended static checking for haskell". Proceedings of the ACM workshop on Haskell: 48. doi:10.1145/1159842.1159849.
- Leino, K. Rustan M. "Extended Static Checking: A Ten-Year Perspective". Informatics. 2000: 157–175. doi:10.1007/3-540-44577-3_11.
- Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg; Saxe, James B. (1998). "Extended Static Checking". Compaq SRC Research Report (159).
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |