Software Systems and Tools
The Formal Methods group has produced a large variety of software tools, both as outcomes of research and also as useful aids to the academic community.
This is a list of links to some of the major products.
The Vampire System
Vampire is a fast and efficient theorem-prover for First-Order Logic.
The Eagle System
Eagle is a rule-based runtime verification framework. Given a finite sequence of program states and a set of formulas written in the temporal logic Eagle, the tool checks if the trace satisfies the set of formulas. The logic Eagle has been designed to allow users define their own recursive temporal operators and then write monitors using those operators. The tool, Eagle Flier, is implemented as a Java library and involves novel techniques for monitoring Eagle formulas. Monitoring is done on a state-by-state basis, without storing the execution trace.
The MSPASS Theorem-prover
The MSPASS theorem prover (Hustadt and Schmidt 2000a) - an enhancement of the first-order theorem prover SPASS with a translator of modal and description logic formulae into first-order logic with equality.
Yarralumla
Yarralumla implements various transformations on clause logic formulas for the purpose of applying first-order bottom-up model generation (BUMG) systems.
The TABSPASS Theorem-prover
The TABSPASS theorem-prover (Hustadt and Schmidt 2000b, Hustadt and Schmidt 2002a) is a modified version of the first-order theorem prover SPASS which simulates derivations of tableaux-based decision procedures for basic modal logic.
The TRP Theorem-prover
The TRP theorem-prover (Hustadt and Schmidt 2001, Hustadt and Schmidt 2002b) is a prototypical implementation of a temporal resolution calculus for propositional linear-time logic.
pdl-tableau
pdl-tableau is a prototypical implementation of the tableau calculus for PDL of De Giacomo and Massacci (2000).
The Agent Dynamic Logic
The Agent Dynamic Logic package - an implementation of algorithms for the reduction of the satisfiability problem in Agent Dynamic Logic (ADL) to the satisfiability problems in CPDL and PDL. Together with any implementation of a decision procedure for PDL or CPDL it gives a prover for ADL.
The SCAN Tool
The SCAN tool is a tool for the elimination of second-order quantifiers; facilitates automated correspondence theory (mentioned on the Page of Positive Reviews of Research in Logical AI).
Empirical analysis of decision procedures for modal logic
There is an empirical analysis of decision procedures for modal logic which does what it says!