# Buchempfehlung zur formalen Verifikation von Programmen

## manuels

Hi,

ich hab mich schon mehrmals gefragt, wie und mit welchen Tools, Computerprogramme formal verifiziert werden.

Leider habe ich bis jetzt im Netz nichts brauchbares gefunden, daher wollte ich mal nachfragen, ob mir jemand von euch einen Buchtipp zu diesem Thema geben kann.

Danke!

Manuel

----------

## schachti

Einen konkreten Buchtipp habe ich nicht, aber "statische Codeanalyse" als Schlagwort. Ein Tool dafür, das ich kenne, ist Polyspace. Vielleicht hilft Dir das schonmal weiter.

----------

## Knieper

 *manuels wrote:*   

> ich hab mich schon mehrmals gefragt, wie und mit welchen Tools, Computerprogramme formal verifiziert werden.

 

Vorwiegend mit Brain 1.0.   :Wink: 

Darauf einzugehen ist nicht ganz einfach, weil ich nicht weiß, welche math. Vorbildung Du hast und welcher Bereich Dich interessiert. Es gibt zig Methoden, Programmeigenschaften zu verifizieren. Du kannst schon vorher das mathematische Modell Deiner Lösung auf bestimmte Eigenschaften prüfen (Model Checker, Process Kalküle), zB. das Protokoll einer Ampelanlage, ob nie zwei kreuzende Fahrbahnen gleichzeitig grün erhalten. Wenn Du dann sicher bist, dass Hardware und Compiler (für beides gibt es auch Verifikationsprojekte) und Protokolle funktionieren, stehst Du vor dem eigentlichen Problem. Entweder Du formulierst Deine Algorithmen und Beweise und generierst die Software (Coq), benutzt Spezifikationssprachen (PVS) oder musst ein Modell für Deine Sprache finden. Bei objektorientierten kann das schwierig werden (Cardelli), man benutzt heute vorwiegend Methoden aus der Kategorientheorie und Coalgebren (Jacobs), bei funktionalen ist es einfacher und man kann sich einfacher Methoden aus der Typtheorie zu nutze machen. Für jede der Methoden braucht man ein breites Fundament aus Logik (zB. Modallogiken, Deduktionssysteme) und diskreter Mathematik. Anwendbar ist das Ganze heutzutage nur für gut spezifizierte kleinere Projekte (Microkerne, Steuerungen, einzelne Module). Etwas praxisnäher ist das sogen. symbolic/concolic testing (Klee) - man nimmt keine konkreten Werte, sondern symbolische, wandert die Pfade in einem Programm ab, hängt dabei versch. Eigenschaften an die Variablen und schaut, ob man damit Fehler (Pointerfehler, asserts...) herbeiführen kann. Ob sich das Programm so verhält, wie man will, weiß man dann natürlich nicht.

Wenn man von all dem keine Ahnung hat und nur eine ganz grobe Vorstellung haben möchte, würde ich empfehlen den (ziemlich alten) Hoare-Kalkül anzugucken und sich die Vorträge um Microsofts Spec# anzusehen. Im Allgemeinen findet man an den Unis Vorlesungsunterlagen, die die Themen abhandeln.

Edit: Mir fiel gerade ein, dass ich mal einen recht einsteigerfreundlichen Artikel gelesen habe: Verifying Red-Black Trees. Erwähnenswert sind noch die bekannten Petri Netze und die relativ "neue" Spieltheorie.

----------

## Knieper

Ok, war vlt. zu viel Text. Relativ neuer Spec#-Artikel: http://research.microsoft.com/en-us/um/people/leino/papers/krml196.pdf

----------

## manuels

Entschuldigung, dass ich mich jetzt erst melde. War schon lang nicht mehr im Gentoo Forum.

Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:

```
for(int i = 0; i < A.rows(); ++i)

#verify: only access A.row(i)

A.row()*x = b;

```

Ich hoffe man versteht, was gemeint ist: Ich möchte in dem Loop verifizieren, dass nur auf die i-te Zeile der Matrix A zugegriffen wird.

----------

## Necoro

 *manuels wrote:*   

> Entschuldigung, dass ich mich jetzt erst melde. War schon lang nicht mehr im Gentoo Forum.

 

Deswegen kann man ja Topics beobachten, auf dass man Mails bekommt wenn sich an denen was ändert. So kann man einige wichtige Sachen im Auge behalten ohne immer das ganze Forum durchforsten zu müssen.

 *Quote:*   

> Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:
> 
> ```
> for(int i = 0; i < A.rows(); ++i)
> 
> ...

 

Mhm - für solche Eigenschaften würde ich in der Tat auch auf "statische Codeanalyse" tippen -- zu mindestens haben wir sowas im Rahmen der Vorlesung "Programmoptimierung" damit gemacht. Allein: Dies wird wohl nicht für den allgemeinen Fall gehen -- aber einer gewissen Komplexität und Pointer-Herumschubserei kann das wohl an seine Grenzen kommen.

/edit: Als Buchempfehlung für den theoretischen Hintergrund würde ich evtl mal das Buch von Flemming Nielson in den Raum stellen

----------

## Knieper

 *manuels wrote:*   

> Hmm, ok. Am liebsten hätte ich wohl solche Verifikationen:
> 
> ```
> for(int i = 0; i < A.rows(); ++i)
> 
> ...

 

Ich kann mit dem Beispiel leider nichts anfangen. Eine Multiplikation auf der linken Seite einer Zuweisung und der Nachweis, dass nur über einen Index zugegriffen wird, dessen Variable nicht mehr auftaucht?! Für Matrizen und dergleichen sind Dependent Types wie in ATS oft ganz hilfreich, mein Fall sind sie nicht so ganz...

----------

