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.
Keywords:
Categories:
Documents:
Please cite this article as follows:
Achim D. Brucker.
Isabelle: Not Only a Proof Assistant. Proof Assistants and Related Tools - The PART Project, 24. sep. 2015. Invited Keynote.
(slides) (handout) (BibTeX) (
| 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.}, | |
| author | = | {Achim D. Brucker}, | |
| day | = | {24}, | |
| event | = | {Proof Assistants and Related Tools - The PART Project}, | |
| handout | = | {https://www.brucker.ch/bibliography/download/2015/talk-brucker-part-isabelle-framework-2015-2x2.pdf}, | |
| isodate | = | {2015-09-24}, | |
| lecturer | = | {Achim D. Brucker}, | |
| location | = | {Lyngby, Denmark}, | |
| month | = | {sep}, | |
| note | = | {Invited Keynote.}, | |
| slides | = | {https://www.brucker.ch/bibliography/download/2015/talk-brucker-part-isabelle-framework-2015.pdf}, | |
| slideshare | = | {key/45EFm5IfekHh8l}, | |
| slideshare_height | = | {355}, | |
| slideshare_width | = | {425}, | |
| title | = | {Isabelle: Not Only a Proof Assistant}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/talk-brucker-part-isabelle-framework-2015}, | |
| year | = | {2015}, |