The formal derivation of algorithm and automatic verification based on Isabelle

DOI10.16357/J.CNKI.ISSN1000-5862.2018.04.10MaRDI QIDQ4624465zbMATH OpenFDO

Authors Leilei Qi, Qinghong Yang, Ying You

Publication date 22 February 2019

Full work available at URL https://doi.org/10.16357/J.CNKI.ISSN1000-5862.2018.04.10

zbMATH Keywords

automatic verificationformal derivationformal methodsIsabelle theorem prover

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 962401
• A formal method for developing algebraic and numerical algorithms
• scientific article; zbMATH DE number 1670746
• Provably correct derivation of algorithms using FermaT
• A system for deduction-based formal verification of workflow-oriented software models

Cited in

(5)

• Integration of formal proof into unified assurance cases with Isabelle/SACM
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• The derivation and formal proof of binary tree sorting non-recursive algorithm
• A formal method for developing algebraic and numerical algorithms
• scientific article; zbMATH DE number 962401 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: The formal derivation of algorithm and automatic verification based on Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4624465)