Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:The Isabelle Refinement Framework
Speaker:Peter Lammich
coming from:TU München
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 21 September 2016
Duration:60 Minutes
Building:E1 4
The idea of top-down refinement is to refine a non-deterministic
specification in several steps to an efficient implementation, and
prove that each step preserves correctness. The stepwise approach is an
important tool to keep different aspects of an algorithm (e.g.
algorithmic ideas and low-level optimizations) separated. This greatly
simplifies correctness proofs, and makes them manageable in first place
for more complex algorithms.

The Isabelle Refinement Framework provides a tool chain for refinement
based top-down development of verified programs, based on the
interactive theorem prover Isabelle/HOL. It has been used for several
verification projects, the largest one being a complete LTL-Model
checker with partial order reduction a la SPIN.

The front end is a shallowly embedded, non-deterministic programming
language, which comes with a refinement calculus and several
convenience tools, like a verification condition generator.

The back end is Imperative/HOL, a shallowly embedded
functional+imperative language, from which Isabelle's code generator
can generate SML/Haskell/Scala/OCaml programs.
Moreover, it comes with a large library of verified data structures and
tool support to simplify their usage.

In this talk, I will give an overview of the Isabelle Refinement
Framework. Knowledge of Isabelle is no prerequisite to understand
(most) of the talk.

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Created by:Jennifer Müller/MPI-INF, 09/16/2016 02:17 PMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Jennifer Müller, 09/16/2016 02:20 PM -- Created document.