Trustworthy Tuesday - Muncake
Albert Rizaldi präsentiert diesen Monat bei Trustworthy Tuesday Muncake!
Veranstaltungsort
Online (Zoom)-, Deutschland
Beschreibung
Trustworthy Tuesday dreht sich diesen Monat alles um Kuchen. Im Rahmen des „Ecosystem Formally Verifiable IT“ (EvIT) präsentiert die GI die Webinar-Reihe „Trustworthy Tuesday“ wieder am 23. Juni.
Albert Rizaldi von PlanV stellt Muncake vor: einen beweisproduzierenden Übersetzer, der Hardware-Modelle, die in HOL4 geschrieben sind, in eine Reihe von Assertions in der Property Specification Language (PSLs) umwandelt, die mit dem kostenlosen und quelloffenen Modellprüfer Yosys überprüft werden können. Wenn diese Behauptungen den Yosys-Modellprüfer bestehen, ist mathematisch garantiert, dass sich das Modell in HOL4 und der RTL-Code gleich verhalten.
Die Verifizierung eines Hardware-Designs anhand eines Referenzmodells ist einfacher und intuitiver als die Konformitätsprüfung anhand einer Reihe von Korrektheitseigenschaften. Dieser modellbasierte Ablauf passt auch gut zu gängigen Entwicklungspraktiken, bei denen ein Design zunächst auf einer höheren Abstraktionsebene beschrieben wird, bevor es zu einer Implementierung verfeinert wird.
Die Veranstaltung findet am 23. Juni ab 14 Uhr (UTC +2) auf Zoom statt. Die Aufzeichnung werden wir nach der Veranstaltung auf die EvIT-Website hochladen.