Extended static checking for Java

By Greg Nelson. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2002

1,552 citations recorded by the source corpus.

Subfields: Information Systems, Software

View Paper: https://www.semanticscholar.org/paper/1cb7df28555b9f220d55357276517068722f0b63

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Information Systems

In Software

Citations in the corpus

VCC: A Practical System for Verifying Concurrent C (2009, result): “Many of these annotations are similar to those found in ESC/Java [8], Spec# [9], or Havoc [10].”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “Work on ESC and Spec# has resulted in important advances on modular heap verification [16, 3].”
Polyglot: An Extensible Compiler Framework for Java (2003, background): “A language might be extended to support annotations necessary for static verification of program correctness [24], more powerful static checking of program invariants [8, 12, 11], or heuristic methods [9].”
A Survey of Automated Techniques for Formal Software Verification (2008, background): “The time and space requirements of procedures for manipulating polyhedra are usually exponential in the number of variables.”
Denali: a goal-directed superoptimizer (2002, methodology): “This approach has been used by the Extended Static Checking research project [3, 13, 6].”
ESC/Java2: Uniting ESC/Java and JML (2004, methodology): “The ESC/Java tool developed at DEC/SRC was a pioneering tool in the application of static program analysis and veriﬁcation technology to annotated Java programs [13].”
Verification of Object-Oriented Programs with Invariants (2003, methodology): “We expect our invariant declarations to be as easy to use as those in ESC/Java [8], but here one needs to explicitly give preconditions about invariants.”
The Daikon system for dynamic detection of likely invariants (2007, methodology): “Extended static checker format for use by the ESC/Java tool [5].”
A comparison of bug finding tools for Java (2004, methodology): “Our study also includes ESC/Java [10], which uses theorem proving, and Bandera [6], which uses model checking.”
PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code (2005, background): “In order to reduce programmers’ effort in manually writing specifications for the extended static type checker (ESC) [12], a tool called Houdini has been developed [11].”
A type and effect system for atomicity (2003, methodology): “ESC/Java has been extended to catch higher-level race conditions, where a stale value from one synchronized block is used in a subsequent synchronized block [9].”
Refinement types for Haskell (2014, background): “Static Contract Checkers like ESCJava [14] are a classical way of verifying correctness through assertions and pre-and post-conditions.”
An overview of JML tools and applications (2003, methodology): “The ESC/Java tool [36], originally developed at Compaq Research, performs what is called extended static checking [27, 60], compile-time checking that goes well beyond typechecking.”
Finding bugs is easy (2004, methodology): “Often, these techniques rely on formal methods and sophisticated program analysis.”
Javert: fully automatic mining of general temporal properties from dynamic traces (2008, methodology): “Temporal API specifications are useful for a number of reasons: they can shorten development time by guiding the production of correct code; they can be used as input to static analysis tools [6, 10, 13, 31] to find bugs automatically; and they can facilitate software maintenance tasks by aiding pro”
Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”