OpenJML

OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. OpenJML is a tool for checking code and specifications of Java programs. We describe our experience building the tool on the foundation of JML, OpenJDK and Eclipse, as well as on many advances in specification-based software verification. The implementation demonstrates the value of integrating specification tools directly in the software development IDE and in automating as many tasks as possible. The tool, though still in progress, has now been used for several college-level courses on software specification and verification and for small-scale studies on existing Java programs.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 6 articles )

Showing results 1 to 6 of 6.
Sorted by year (citations)

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  3. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  4. Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N.: AutoProof: Auto-active Functional Verification of Object-oriented Programs (2015) arXiv
  5. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  6. Anureev, I. S.: Integrated approach to analysis and verification of imperative programs (2011)