Links to Related Web Pages
- The sourceforge.net project page for JML.
- The ESC/Java2 project, led by Joe Kiniry and David Cok.
- The AutoGrader, Beetlz, BONc, FreeBoogie, KOA, Mobius Program Verification Environment (PVE), RCC, and SenseTile projects, led by Joe Kiniry.
- The Extended Static Checking project at Compaq Systems Research Center. You can also get the Source release of ESC/Java now.
- LOOP project from Bart Jacobs's group in Nijmegen.
- the Daikon invariant detector project from Michael D. Ernst's group at MIT.
- The ChAsE tool for statically checking the modifiable/assignable clauses in the ESC/Java subset of JML specifications, by Néstor Cataño Collazos at INRIA Sophia-Antipolis.
- Java Applet Correctness Kit which is an industrial use of JML.
- JML specification extensions with Bogor, a project doing model checking of JML specifications at Kansas State University.
- Project to port the JML tools to Eclipse at Kansas State University and elsewhere.
- The KeY Project, project that aims to "integrate formal software specification and verification into the industrial software engineering processes". They also have a JML front end.
- The Generation of Certified Code for Object Oriented Applications (GECCOO) project, which involves specification, refinement, proof and error detection and some tools for JML.
- Commands to use the syntax highlighting feature of VIM for JML specifications by Engelbert Hubbers from Nijmegen
- JAG: a JML Annotation Generation for Verifying Temporal Properties.
- Jutil.org which is a "high-quality API for general utility code" specified using JML.
- The Bytecode Modeling Language (BML) a variant of JML at the bytecode level.
- iContract, which supports specifications in javadoc comments.
- CnC: Check 'n' Crash
- iDoclet, the iContract doclet and other iContract add-ons.
- Modern Jass (Java with assertions), which supports design by contract for Java. This supercedes the older version of Jass, and is more closely related to JML.
- jContractor, an open-source tool that supports design by contract for Java.
- Contract4j, a design by contract language for Java 5, using Java annoations, and implemented using aspect-oriented technology.
- J-LO (the Java Logical Observer), a language that allows Linear Temporal Logic (LTL) Formulas to be expressed over AspectJ pointcuts. The tool checks them at runtime.
- Fluid, a project building tools to automatically check non-local properties of Java programs.
- ConGu checks Java code against "property-driven algebraic specifications".
- Jcontract and Jtest tools for design by contract and unit testing from Parasoft Corporation.
- Perfect Developer for Java and C++ from Eschertech.
- The Infospheres Java Coding Standard.
- Doclets written in Javadoc, some of which pertain to specification.
- DowWiz - The JavaDoc Documentation Tool
- JUnit for Java test cases.
- Test Mentor for Java.
- The T2 testing framework
- Java PathFinder a model checker for Java programs, which is also now an sourceforge.net project.
- The Verification Software Environment (VSE) from the formal method group at the Deutsches Forschungszentrum für Künstliche Intelligenz Saarbrücken, Germany.
- Findbugs, a tool for finding bugs in Java code.
- Bandera a model checker and model checking framework for Java programs.
- Nully plugin for the IDEA programming environment that checks @NonNull annotations.
- Spec# a specification language similar to JML for C#.
- nContract, a specification language using .NET annotations, with model fields and pure methods.
- ANSI/ISO C Specification Language (ACSL), a specification language for C that is "largely inspired by JML".
- Eiffel.com, which features various Eiffel software tools and documentation about Eiffel.
- SmartEiffel the GNU Eiffel compiler from SmartEiffel.loria.fr, home of open source Eiffel tools.
- Sage, a language with an expressive type system that includes specifications that are run-time checked.
- Mocha model checker home page.
- Alloy Analyzer, an object modeling notation and lightweight formal method.
- MulSaw project web page.
- OCL, the Object Constraint Language of the UML.
- Self-Testable Classes and Design for Testability web site by D. Deveaux, J-M. Jezequel and Y. Le Traon.
- Hyper/J, a tool supporting "multi-dimensional separation of concerns" for Java.
- AspectJ, aspect-oriented programming for Java.
- Demeter and DJ.
- Other Java tools (from JavaWorld).
- JSwat Java debugger.
- The Jacks (Java compiler Killer System)
- The Larch FAQ.
- The VDM Portal.
- IFAD's site for VDM-SL and related tools.
- Foundations of software engineering group at Microsoft Research, including the Abstract State Machine Language (AsmL).
- Blue, a teaching language that incorporates formal specification constructs.
- The World-Wide Web Virtual Library: Formal Methods
Last modified Monday, November 16, 2009.