AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

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.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only