Documentation and Publications
ESC/Java2 comes with a copious amount (hundreds of pages) of documentation.
Booklets
- The original SRC ESC/Java User's Guide
The information in the original Users's Guide is still accurate, except where superseded by the data in the Implementation Notes or by recent updates to this website.
- ESC/Java2 Implementation Notes
- Extending ESC/Java2
- The Logics and Calculi of ESC/Java2
- The Provers of ESC/Java2
- ESC/Java2 also comes with all the original SRC ESC/Java design notes.
Papers
- Soundness and Completeness Warnings in ESC/Java2 (posted when final version submitted)
- Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2
- ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system
- Reasoning with specifications containing method calls in JML and first-order provers
- ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2
Slides
- ESC/Java: Extended Static Checking for Java
- Introduction to JML
- ESC/Java2: Use and Features
- ESC/Java2 Warnings
- Specification Tips and Pitfalls
- Advanced JML (and more Tips and Pitfalls)
- ESC/Java: Extended Static Checking for Java (a summary and non-interactive demonstration)
- Effectively Using JML: Software Engineering Processes incorporating Formal Specification
- Using ESC/Java2 Architecture, Hints, and Tricks
- Using Formal Methods for VLSI Development: Using Java and JML in the Real World
- Models are the `M' in JML: Using ADT Models in Formal Specification with JML
- The ESC/Java2 Calculi and Object Logics: Implications on Specification and Verification