Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation

Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation

Mechanical theorem proving is especially advantageous on formal verification of algorithms manipulating complicated data structures. Some proof assistants such as Isabelle/HOL also enable users to extract executable code from verified specification, pushing the correctness assurance from algorithm l...

Full description

Bibliographic Details
Main Authors: Haitao Wang, Lihua Song
Format: Article
Language:English
Published: IEEE 2021-01-01
Series:IEEE Access
Subjects:
Code generation
file comparison algorithm
formal verification
interactive theorem proving
Isabelle/HOL
Online Access:https://ieeexplore.ieee.org/document/9348915/

Internet

https://ieeexplore.ieee.org/document/9348915/

Similar Items