Extended Static Checking for Java

13 years 11 months ago
Extended Static Checking for Java
Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theoremproving techniques. It provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. ESC/Java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. This paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of Java programs. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/Sp...
Greg Nelson
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where MPC
Authors Greg Nelson
Comments (0)