ESC/Java2: Uniting ESC/Java and JML
By David R. Cok, Joseph R. Kiniry. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2004
295 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/28fdbd8f308e714e81ee2e3919debed1912659f2
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- François Bobot
- A. Paskevich
- Jean-Christophe Filliâtre
- Claude Marché
- M. Leino
- K. Rustan
- Danfeng Zhang
- Daniel Kifer
In Computational Theory and Mathematics
- François Bobot
- A. Paskevich
- Jean-Christophe Filliâtre
- Claude Marché
- M. Leino
- K. Rustan
- Daniel Kifer
- Danfeng Zhang
Citations in the corpus
- Dafny: An Automatic Program Verifier for Functional Correctness (2010, methodology): “ESC/Java [22,15] uses JML specifications and uses an underlying SMT solver, but it performs extended static checking (that is, it intentionally misses some program errors in order to reduce the cost of using the tool [19]), not full verification.”
- Why3: Shepherd Your Herd of Provers (2011, background): “This is the case of VCC [12], Spec# [2], Dafny [19], Chalice [20], ESC/Java2 [11], Krakatoa [21], Frama-C [15].”