FME Formal Methods Tools Database - Formal Methods Europe (FME) is a European organization, supported by the Commission of the European Union, with the mission of promoting and supporting the industrial use of formal methods for computer systems development.
Semantic Designs, Incorporated - Semantic Designs produces the Design Maintenance System (DMS), a software engineering environment that supports the incremental construction and maintenance of large application systems and is driven by semantics and captured designs. DMS records what the software is supposed to do (specification), how the software does it (the code), and why the software works correctly (the design). Using practical program generation and transformation technology, DMS will enable designers to understand the design, and modify the design to obtain new code.
This site allows visitors to Download a FREE evaluation version of the CloneDR: an easy-to-use tool that detects and automatically removes duplicate code from source programs in C, C++, Java or COBOL or any other text-based computer language.
Tool Support for Fine-Grained Software Inspection - Software inspection is a proven technique to improve quality and reduce costs. Detailed source code inspections are an important part of the formal inspection process, but they require a significant time investment. Research advances in static program analysis can reduce the inspection time required. By calculating answers to standard inspection questions, CodeSurfer frees experts to focus their efforts on more challenging inspection issues. CodeSurfer provides access to and answers queries about the system-dependence graph representation of programs, and can be integrated with other tools.
TorX - Developed at the Formal Methods and Tools research group at the University of Twente (UT) in the Netherlands, the TorX tool is a prototype testing tool for conformance testing of reactive software. The tool requires a real implementation and a (formal) specification of that implementation. The specification describes system behaviour that the real implementation is allowed to perform. The TorX tool is the arbiter that checks the correct behaviour of a real implementation during its execution based on the formal specification.
UniTesK Methodology - Unified Testing & specification toolkit takes input from LOTOS, PROMELA, or SDL models for the automated generation of Test Suites from Formal Specifications.
DACS Gold Practice Initiative
