We provide the following list of related sites as a service to those interested in formal methods. If you think something important is missing, please drop us a line.
Compilations, Digital Libraries, etc.
- The World Wide Web Library: Formal Methods
- This excellent, comprehensive reference site is organized by Jonathan Bowan.
Software for Correct Software
- Programming Languages
- Eiffel is widely considered to be the premire widely used OO language available today.
- Haskell is a purely functional programming language.
- Mercury is a new logic/functional programming language, which combines the clarity and expressiveness of declarative programming with advanced static analysis and error detection features. Its highly optimized execution algorithm delivers efficiency far in excess of existing logic programming systems, and close to conventional programming systems.
- Objective Caml
- Objective Caml (or OCaml for short) is the latest implementation of the Caml dialect of ML. Its main novelties are full support for objects and classes, a powerful module calculus, and a very high-performance native code compiler.
- Programming or Proof Tools
- A multi-language, open source UML-centric CASE tool.
- ESCJava: Extended Static Checking for Java
- The Compaq Extended Static Checker for Java (ESC/Java), developed at the Compaq Systems Research Center (SRC), is a programming tool for finding errors in Java programs. ESC/Java detects, at compile time, common programming errors that ordinarily are not detected until run time, and sometimes not even then; for example, null dereference errors, array bounds errors, type cast errors, and race conditions.
- Jass: Java with Assertions
- Jass is a precompiler that supports assertions for Java. The concepts of design by contract from Bertrand Meyer have been transferred to Java and extended with new features.
- The Java Modeling Language (JML)
- The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the approaches of Eiffel and Larch, with some elements of the refinement calculus.
- A research group and toolsuite for developing correct Java programs via formal methods. The LOOP tools is a compiler which translates classes in object-oriented languages into logical theories for use in proof tools like PVS and Isabelle.
- The Proof General
- Proof General is a generic interface for proof assistants, currently based on Emacs. It has been developed at the LFCS in the University of Edinburgh.
- The Dresden OCL Compiler hosted at SourceForge
- A compiler and Java code generator for the Object Constraint Language (OCL).
- The main purpose of Emacs package X-Symbol is to provide some WYSIWYGness in an area where it greatly enhance the readability of your LaTeX or HTML source: using "real" characters for "tokens" like \oplus or ™. It also provides input methods for these characters, both for the beginner and the expert (some users regard this as the main reason to use package x-symbol). WYSIWYG super- and subscripts and images/figures are also supported.
- Logical Frameworks and Theorem Provers
- The Coq tool is a proof assistant which: helps manipulate a calculus of assertions, mechanically checks proofs of these assertions, helps find formal proofs, extracts certified programs from constructive proofs of their formal specifications.
- The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses from formalizing pure mathematics to verification of industrial hardware.
- Isabelle is a popular generic theorem proving environment developed at Cambridge University and TU Munich.
- Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications.
- PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications.