Otoni, RodrigoReischuk, Rüdiger2024-10-022024-10-022024978-3-88579-982-5https://dl.gi.de/handle/20.500.12116/44715Blockchain-Technologien haben sowohl in der Wissenschaft als auch in der Industrie große Aufmerksamkeit auf sich gezogen. Da sie als Mittel zum Halten und Manipulieren von Finanzwerten verwendet werden, sind sie ein beliebtes Ziel von Angriffen. In der Vergangenheit sind bereits Vermögenswerte in der Größenordnung von Millionen von US-Dollar verloren gegangen. Vor diesem Hintergrund ist die Fähigkeit, sicherzustellen, dass keine Schwachstellen vorhanden sind, von entscheidender Bedeutung. Die hier zusammengefasste Dissertation stützt sich auf die jüngsten Fortschritte im Bereich der symbolischen Modellprüfung, insbesondere auf Techniken, die auf Satisfiability Modulo Theories (SMT) und Constrained Horn Clauses (CHC) basieren, um den Bedarf an einer automatisierten Überprüfung von Blockchain-Technologien zu decken. Der Blockchain- Bereich wird sowohl auf der Plattform- als auch auf der Anwendungsebene durch TLA+-Spezifikationen und Solidity-Smart-Contracts angegangen, und die Verwendung von Korrektheitszeugnissen zur Zertifizierung der Ergebnisse von Solvern, die für die betreffenden Logikfragmente bestimmt sind, wird als Mittel zur Gewährleistung der Korrektheit untersucht.de10.18420/Diss2023-19