Entwicklung eines korrekten Assemblierers. Sekerinski, E. Ph.D. Thesis, Universität Karlsruhe, 1989.
Entwicklung eines korrekten Assemblierers [pdf]Paper  abstract   bibtex   
In dieser Arbeit wird ein Assemblierer für den MC68020 Prozessor entwickelt und gegenüber einer formalen Spezifikation als korrekt bewiesen. Die Spezifikation ist in Prädikatenlogik gegeben, und die angewandte Beweismethode ist ein auf Prädikatenlogik aufgesetzter Kalkül. Die Implementierung ist in Modula-2 geschrieben und hat, neben ihrer Korrektheit, die Vorzüge, extrem kompakt und effizient zu sein.

Downloads: 0