Project Details
Description
Investigations and experiments with the purpose of constructing a practically applicable, computer based proof tool for reasoning about VDM-SL specifications.
In particular construction of a prover for the logic LPF, by use of the generic proof tool Isabelle and translators between the full VDM-SL and the core language which is supported by the LPF prover.
In particular construction of a prover for the logic LPF, by use of the generic proof tool Isabelle and translators between the full VDM-SL and the core language which is supported by the LPF prover.
| Status | Finished |
|---|---|
| Effective start/end date | 01/01/1996 → 30/08/1997 |