Verified software

Opening & welcome
Dines Bjørner
Prof. Emer Detrekői Ákos 15 éve - 11:49

The ideal of program correctness

A million lines of verified code

Have we learned from the Wasa disaster?

Temporal annotations and their validation

The German VeriSoft Project 2003-2007

Model checking, theorem proving, and abstract
