Verified software

Opening & welcome
Dines Bjørner
Prof. Emer Ákos Detrekői 15 years ago - 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
