RISC » FORMSEM04
 
 
Weekly outline
 
In this seminar, we will investigate methods and software for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...).

Each participant is expected to contributed in some way or another, e.g. to study e.g. one particular software system, install it at RISC, and give a presentation on it.

Of course, people just interested in listening to the presentations are also cordially invited!

Forum News forum
 
8
24 November - 30 November
  1. Talk by Franz Lichtenberger on Symposium on Teaching Formal Methods 2004
  2. Talk by Laura Kovacs on "Generating Loop Invariants for Imperative Program Verifcation in Theorema".
Resource Generating Loop Invariants in Theorema