VDM recursive functions in Isabelle/HOL
Leo Freitas, Peter Gorm Larsen
TL;DR
This paper presents an extension of a translation tool from VDM-SL to Isabelle/HOL, focusing on recursive functions, to facilitate formal verification using higher-order logic.
Contribution
It introduces an extended translation and a VDM mathematical toolbox in Isabelle/HOL supporting recursive functions, enhancing formal verification capabilities.
Findings
Extended translation supports recursive functions in Isabelle/HOL
Development of a VDM mathematical toolbox in Isabelle/HOL
Facilitates formal verification of recursive functions
Abstract
For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isabelle/HOL enabling support for recursive functions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Logic, programming, and type systems · Formal Methods in Verification