The WWW Virtual Library: Formal Methods
Pointers to information on Formal Methods, useful for mathematically describing and reasoning about computer-based systems.
StateWORKS Studio
Professional software specification environment based on finite state machine (FSM) concept. Contains FSM editor, simulator, monitoring and debugging tools. Allows to build complex FSM systems. For WindowsNT/2000/XP operating systems.
Statestep
A lightweight, systematic method for finite state machine specification: a tool includes interactive checking and a kind of spreadsheet for invariants; it also supports decision tables and combinatorial completion.
ResearchIndex: Structure-preserving specification languages for knowledge-based systems
Much work on validation and verification of knowledge based systems (KBSs) has been done in implementation languages, mostly rule based. Recent papers suggest it is useful to do validation and verification in a more abstract and formal specification of the system.
ResearchIndex: Proof Theoretic Approach To Specification Languages
Thesis studies FORUM as specification language. FORUM is a higher order logic based on the logical connectives of Linear Logic. Initial example demonstrates that FORUM is well suited to specify concurrent computations by specifying the higher order ß calculus.
KORSO
Deduction oriented Development of Specifications: language designed for modularizing large projects. Complex specifications can be hierarchically structured by combining specifications with renaming and hiding. Powerful enough to express implementation of specifications via more primitive specifications.
Interactive Software Development and Renovation Software
ASF+SDF compiler runtime library, Meta-Environment, ATerm Library, SDF2 Parser generator, Completa, SGLR (Scannerless Generalized LR parser), ToolBus.
INKA Inductive Theorem Prover
First-order theorem prover with induction based on the explicit induction paradigm. It is based on a full first-order calculus, a special variant of the resolution calculus with paramodulation.
HasCASL DFG Project
Algebraic Specification + Functional Programming = Environment for Formal Software Development. An extension of CASL that establishes a connection with the functional programming language Haskell.
FraCaS
A Framework for Computational Semantics.
[ 1 ] [ 2 ]
|
