pdfreaders.org

Isabelle: Not Only a Proof Assistant

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.

Schlüsselwörter:
Kategorien:
Dokumente:

QR Code for talk:brucker:part-isabelle-framework:2015.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker. Isabelle: Not Only a Proof Assistant. Proof Assistants and Related Tools - The PART Project, 24. sep. 2015. Invited Keynote.
(Folien) (Handout) (BibTeX) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@Talk{ talk:brucker:part-isabelle-framework:2015,
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},
}