Isabelle: Not Only a Proof Assistant

By Achim D. Brucker.

The Isabelle homepage describes Isabelle as "a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus." While this, without doubts, what most users of Isabelle are using Isabelle for, there is much more to discover: Isabelle is also a framework for building formal methods tools.

In this talk, I will report on our experience in using Isabelle for building formal tools for high-level specifications languages (e.g., OCL, Z) as well as using Isabelle’s core engine for new applications domains such as generating test cases from high-level specifications.

Please cite this work as follows:
A. D. Brucker, “Isabelle: Not only a proof assistant,” presented at the Proof assistants and related tools - the PART project, Lyngby, Denmark, Sep. 24, 2015. Invited Keynote.. Author copy: https://logicalhacking.com/publications/talk-brucker-part-isabelle-framework-2015/

BibTeX
@Unpublished{ talk:brucker:part-isabelle-framework:2015,
  date              = {2015-09-24},
  title             = {Isabelle: Not Only a Proof Assistant},
  author            = {Achim D. Brucker},
  note              = {Invited Keynote.. 
                       Author copy: \url{https://logicalhacking.com/publications/talk-brucker-part-isabelle-framework-2015/}},
  venue             = {Lyngby, Denmark},
  year              = {2015},
  eventtitle        = {Proof Assistants and Related Tools - The PART Project},
  abstract          = {The Isabelle homepage describes Isabelle as "a generic proof
                       assistant. It allows mathematical formulas to be expressed in
                       a formal language and provides tools for proving those
                       formulas in a logical calculus." While this, without doubts,
                       what most users of Isabelle are using Isabelle for, there is
                       much more to discover: Isabelle is also a framework for
                       building formal methods tools.
                       
                       In this talk, I will report on our experience in using
                       Isabelle for building formal tools for high-level
                       specifications languages (e.g., OCL, Z) as well as using
                       Isabelle's core engine for new applications domains such as
                       generating test cases from high-level specifications.},
  slideshare        = {key/45EFm5IfekHh8l},
  slideshare_width  = {425},
  slideshare_height = {355},
  pdf               = {https://logicalhacking.com/publications/talk-brucker-part-isabelle-framework-2015/talk-brucker-part-isabelle-framework-2015.pdf},
}