@misc{Klasen2010,
  author    = {Klasen, Volker},
  title     = {Verifying Dijkstra's Algorithm with KeY},
  url       = {https://nbn-resolving.org/urn:nbn:de:kola-4203},
  institution = {Institut f{\"u}r Informatik},
  pages     = {iv, 69},
  year      = {2010},
  abstract  = {Die Entwicklung von Algorithmen im Sinne des Algorithm Engineering geschieht zyklisch. Der entworfene Algorithmus wird theoretisch analysiert und anschließend implementiert. Nach der praktischen Evaluierung wird der Entwurf anhand der gewonnenen Kenntnisse weiter entwickelt. Formale Verifffizierung der Implementation neben der praktischen Evaluierung kann den Entwicklungsprozess verbessern. Mit der Java Modeling Language (JML) und dem KeY tool stehen eine einfache Spezififfkationssprache und ein benutzerfreundliches, automatisiertes Verififfkationstool zur Verf{\"u}gung. Diese Arbeit untersucht, inwieweit das KeY tool f{\"u}r die Verifffizierung von komplexeren Algorithmen geeignet ist und welche R{\"u}ckmeldungen f{\"u}r Algorithmiker aus der Verififfkation gewonnen werden k{\"o}nnen.Die Untersuchung geschieht anhand von Dijkstras Algorithmus zur Berechnung von k{\"u}rzesten Wegen in einem Graphen. Es sollen eine konkrete Implementation des Standard-Algorithmus und anschließend Implementationen weiterer Varianten verifffiziert werden. Dies ahmt den Entwicklungsprozess des Algorithmus nach, um in jeder Iteration nach m{\"o}glichen R{\"u}ckmeldungen zu suchen. Bei der Verifffizierung der konkreten Implementation merken wir, dass es n{\"o}tig ist, zuerst eine abstraktere Implementation mit einfacheren Datenstrukturen zu verififfzieren. Mit den dort gewonnenen Kenntnissen k{\"o}nnen wir dann die Verifikation der konkreten Implementation fortf{\"u}hren. Auch die Varianten des Algorithmus k{\"o}nnen dank der vorangehenden Verififfkationen verifiziert werden. Die Komplexit{\"a}t von Dijkstras Algorithmus bereitet dem KeY tool einige Schwierigkeiten bez{\"u}glich der Performanz, weswegen wir w{\"a}hrend der Verifizierung die Automatisierung etwas reduzieren m{\"u}ssen. Auf der anderenrn Seite zeigt sich, dass sich aus der Verifffikation einige R{\"u}ckmeldungen ableiten lassen.},
  language  = {en}
}