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 |
Collaborative partners
- Technical University of Denmark (lead)
- Institut for Anvendt Datalogi (Project partner)
Funding
- Unknown
Fingerprint
Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.