Verification of Object-Oriented Programs with Invariants
By Mike Barnett, R. Deline, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte. Journal of Object Technology, 2003
396 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/26689cbd6fc9d5d3404497bcc1aa6886bd1ceb2c
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
- Cristiano Calcagno
- Peter W. O'Hearn
- Hongseok Yang
- Josh Berdine
- M. Leino
- K. Rustan
- Wolfram Schulte
- Mike Barnett
In Computational Theory and Mathematics
- Cristiano Calcagno
- Peter W. O'Hearn
- Hongseok Yang
- Josh Berdine
- M. Leino
- K. Rustan
- Wolfram Schulte
- David R. Cok
Citations in the corpus
- Local Action and Abstract Separation Logic (2007, background): “The work on Boogie [2] achieves modularity using ideas that have hints of the primitives in separation logic [21], and a study of the abstract principles underlying Boogie could be valuable.”
- An overview of JML tools and applications (2003, background): “Spec# and JML is that Spec# builds in a new methodology for object invariants [5, 7, 63], trading restrictions on the kinds of programs that can be written for a sound modular reasoning technique.”
- The Spec# Programming System: An Overview (2004, methodology): “Our methodology for object invariants and modifies clauses relies on object ownership to impose a structure on the heap [3, 45, 6].”
- Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “A recent emphasis has been on using ownership assertions that refer to auxiliary fields that may be altered, and this leads to added flexibility [2, 24], including transfer.”